1 (* Title: "BridgeJEdit/vscode-example.sml"
3 (c) due to copyright terms
6 "-----------------------------------------------------------------------------------------------";
7 "table of contents -----------------------------------------------------------------------------";
8 "-----------------------------------------------------------------------------------------------";
9 "-----------------------------------------------------------------------------------------------";
10 "----------- VSCode example with Step.specify_do_next ------------------------------------------";
11 "-----------------------------------------------------------------------------------------------";
12 "-----------------------------------------------------------------------------------------------";
13 "-----------------------------------------------------------------------------------------------";
15 (**** VSCode example with Step.specify_do_next ########################################### ****)
16 "----------- VSCode example with Step.specify_do_next ------------------------------------------";
17 "----------- VSCode example with Step.specify_do_next ------------------------------------------";
21 "Constants [r = (7::real)]", "Maximum A", "AdditionalValues [u, v]",
22 "Extremum (A = 2 * u * v - u \<up> 2)",
23 "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]",
24 "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]",
25 "SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]",
27 "FunctionVariable a", "FunctionVariable b", "FunctionVariable \<alpha>",
30 "Domain {0 <..< \<pi> / 2}",
31 "ErrorBound (\<epsilon> = (0::real))"
32 ]: TermC.as_string list;
33 if (fmz |> map (TermC.parseNEW @{context}) |> filter is_some |> length) = 14
34 then () else error "Formalise.model not parsed completely";
37 ("Diff_App", ["univariate_calculus", "Optimisation"], ["Optimisation", "by_univariate_calculus"]);
39 (*/------- start example as usual in tests ---------------------------------------------------* )
40 val (p,_,f, nxt,_,pt) = CalcTreeTEST [(fmz, refs)];
42 ( *-------- outcomment EITHER above OR below --------------------------------------------------*)
43 case Store.get (KEStore_Elems.get_expls @{theory}) ["Diff_App-No.123a"] ["Diff_App-No.123a"] of
44 (_, ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" :: _,
45 ("Diff_App", ["univariate_calculus", "Optimisation"] ,["Optimisation", "by_univariate_calculus"])))
47 | _ => error "intermed. example_store CHANGED";
49 val pt = update_state (*here we have Ctree.EmptyPtree and thus call init_ctree*)
51 (* Problem.parse_model_input results in markup, which is accepted by \<open>fun update_state\<close>, too:
52 Constants [r = 7] *)
53 ( [("#Given", ["Constants [r = 7]"]),
54 ("#Where", ["0 < r"]),
55 ("#Find", ["Maximum A", "AdditionalValues [u, v]"]),
56 ("#Relate", ["Extremum A = 2 * u * v - u \<up> 2",
57 "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]"])
59 ("Diff_App", ["univariate_calculus", "Optimisation"], ["Optimisation", "by_univariate_calculus"])
60 (*References_Def.explode_id ^^^^^^^^^^^^^^^^^^^^^^, ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
64 (*\------- start example as required in VSCode_Example.thy -----------------------------------*)
66 (*** stepwise Specification: Problem model================================================= ***)
67 (** ) we drop this step, because the user shall be presented a (empty) Model ... ( ** )
68 val ("ok", ([(Model_Problem, Model_Problem' (["univariate_calculus", "Optimisation"], _, _), _)], _, ptp))
69 = Step.specify_do_next ptp;
71 val ("ok", ([(Tactic.Add_Given "Constants [r = 7]", _, _)], _, ptp))
72 = Step.specify_do_next ptp;
73 val ("ok", ([(Tactic.Add_Find "Maximum A", _, _)], _, ptp))
74 = Step.specify_do_next ptp;
75 val ("ok", ([(Tactic.Add_Find "AdditionalValues [u]", _, _)], _, ptp))
76 = Step.specify_do_next ptp;
77 val ("ok", ([(Tactic.Add_Find "AdditionalValues [v]", _, _)], _, ptp))
78 = Step.specify_do_next ptp;
79 val ("ok", ([(Tactic.Add_Relation "Extremum (A = 2 * u * v - u \<up> 2)", _, _)], _, ptp))
80 = Step.specify_do_next ptp;
81 val ("ok", ([(Tactic.Add_Relation "SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]", _, _)], _, ptp))
82 = Step.specify_do_next ptp;
84 (*** Problem model is complete ============================================================ ***)
85 val PblObj {probl, ...} = get_obj I (fst ptp) [];
86 if I_Model.to_string @{context} probl = "[\n" ^
87 "(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] ,(fixes, [[r = 7]])), \n" ^
88 "(2 ,[1, 2, 3] ,true ,#Find ,Cor Maximum A ,(maxx, [A])), \n" ^
89 "(3 ,[1, 2, 3] ,true ,#Find ,Cor AdditionalValues [u, v] ,(vals, [[u, v]])), \n" ^
90 "(4 ,[1, 2, 3] ,true ,#Relate ,Cor Extremum (A = 2 * u * v - u \<up> 2) ,(extr, [A = 2 * u * v - u \<up> 2])), \n" ^
91 "(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]]))]"
92 then () else error "I_Model.to_string probl CHANGED";
94 (*//---------------- adhoc inserted ------------------------------------------------\\*)
96 (* already been input -------vvvvvvvvvvvvvvvvvvv: code in check_input is missing*)
97 (*+*)val ("ok", ([(Tactic.Add_Given "Constants [r = 7]", _, _)], _, ptp))
98 = (**) Step.specify_do_next ptp;
100 (*+*)val ("ERROR I_Model.check_single: \"Maximum A\"\" not for field \"#Find\"", ([], [], ptp))
101 = (**) Step.specify_do_next ptp;
102 (*\\---------------- adhoc inserted ------------------------------------------------//*)
104 (*** Specification of References ========================================================== *** )
105 val ("ok", ([(Specify_Theory "Diff_App", _, _)], _, ptp))
106 = Step.specify_do_next ptp;
107 val ("ok", ([(Specify_Problem ["univariate_calculus", "Optimisation"], _, _)], _, ptp))
108 = Step.specify_do_next ptp;
109 val ("ok", ([(Specify_Method ["Optimisation", "by_univariate_calculus"], _, _)], _, ptp))
110 = Step.specify_do_next ptp;
111 ---------------------------------------------------------------------- trace from CalcTreeTEST*)
113 (*** stepwise Specification: MethodC model ================================================ ***
115 val ("ok", ([(Add_Given "FunctionVariable a", _, _)], _, ptp))
116 = Step.specify_do_next ptp;
117 val ("ok", ([(Add_Given "Input_Descript.Domain {0<..<r}", _, _)], _, ptp))
118 = Step.specify_do_next ptp;
119 val ("ok", ([(Add_Given "ErrorBound (\<epsilon> = 0)", _, _)], _, ptp))
120 = Step.specify_do_next ptp;
121 ---------------------------------------------------------------------- trace from CalcTreeTEST*)
123 (*** Specification of Problem and MethodC model is complete =============================== ***)
124 val PblObj {meth, ...} = get_obj I (fst ptp) [];
125 (*with update_state*)
126 if I_Model.to_string @{context} meth = ("[\n" ^
127 "(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] ,(fixes, [[r = 7]]))]"
128 ) then () else error "ERROR output CHANGED";
130 (*with CalcTreeTEST* )
131 if I_Model.to_string @ {context} meth = "[\n" ^
132 "(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] ,(fixes, [[r = 7]])), \n" ^
133 "(2 ,[1, 2, 3] ,true ,#Find ,Cor Maximum A ,(maxx, [A])), \n" ^
134 "(3 ,[1, 2, 3] ,true ,#Find ,Cor AdditionalValues [u, v] ,(vals, [[u, v]])), \n" ^
135 "(4 ,[1, 2, 3] ,true ,#Relate ,Cor Extremum (A = 2 * u * v - u \<up> 2) ,(extr, [A = 2 * u * v - u \<up> 2])), \n" ^
136 "(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" ^
137 "(7 ,[1] ,true ,#Given ,Cor FunctionVariable a ,(funvar, [a])), \n" ^
138 "(10 ,[1, 2] ,true ,#Given ,Cor Input_Descript.Domain {0<..<r} ,(doma, [{0<..<r}])), \n" ^
139 "(12 ,[1, 2, 3] ,true ,#Given ,Cor ErrorBound (\<epsilon> = 0) ,(err, [\<epsilon> = 0]))]"
140 then () else error "I_Model.to_string meth CHANGED";
141 ---------------------------------------------------------------------- trace from CalcTreeTEST*)
143 (*** Solution starts ====================================================================== ***)
145 Step.specify_do_next ptp;
146 (*ERinROR in creating the environment from formal args. of partial_function "Diff_App.univar_optimisation"
147 and the actual args., ie. items of the guard of "["Optimisation", "by_univariate_calculus"]" by "assoc_by_type":
148 formal arg "err" of type "bool" doesn't mach an actual arg.
150 7 formal args: ["fixes", "maxx", "extr", "sideconds", "funvar", "doma", "err"]
151 7 actual args: ["[r = 7]", "A", "[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]", "a", "{0<..<r}", "\<epsilon> = 0", "[u, v]"]
152 with types: ["bool list", "real", "bool list", "real", "real set", "bool", "real list"]*)