1.1 --- a/README.md Tue Jul 26 22:11:41 2022 +0200
1.2 +++ b/README.md Tue Jul 26 22:29:35 2022 +0200
1.3 @@ -70,4 +70,5 @@
1.4 ====isabisac2$ ./bin/isabelle jedit -l HOL ../isa2/src/Tools/isac/Build_Isac.thy &
1.5 * Parallel Test
1.6 ====isabisac2$ ./bin/isabelle jedit -l Isac_Test_Base ../isa2/test/Tools/isac/Test_Isac_Short.thy &
1.7 +====isabisac2$ ./bin/isabelle jedit -l Isac_Test_Base ../isa2/test/Tools/isac/Test_Some.thy &
1.8
2.1 --- a/TODO.md Tue Jul 26 22:11:41 2022 +0200
2.2 +++ b/TODO.md Tue Jul 26 22:29:35 2022 +0200
2.3 @@ -97,4 +97,13 @@
2.4 - this proposal presumable involves hacking of parsers -- is there a better way?
2.5 - implementation and tests have solution for (a) above as a prerequisite.
2.6
2.7 +* WN: rename in Formalise: type spec = Model_Def.form_spec;
2.8 + type refs = Model_Def.form_refs;
2.9 +* WN: rename in Know_Store: get_ptyps, add_pbts
2.10 + get_pbls, add_pbls
2.11 +* WN: rename in References_Def: select
2.12 + select_new
2.13 +* WN: as soon as parsing in Outer_Syntax.command..‹Example› works, implement in Calculation
2.14 + - init_ctree, update_status, check_input
2.15
2.16 +
3.1 --- a/test/Tools/isac/BridgeJEdit/vscode-example.sml Tue Jul 26 22:11:41 2022 +0200
3.2 +++ b/test/Tools/isac/BridgeJEdit/vscode-example.sml Tue Jul 26 22:29:35 2022 +0200
3.3 @@ -33,24 +33,52 @@
3.4 if (fmz |> map (TermC.parseNEW @{context}) |> filter is_some |> length) = 14
3.5 then () else error "Formalise.model not parsed completely";
3.6
3.7 -val refs =
3.8 +val refs =
3.9 ("Diff_App", ["univariate_calculus", "Optimisation"], ["Optimisation", "by_univariate_calculus"]);
3.10 +
3.11 +(*/------- start example as usual in tests ---------------------------------------------------* )
3.12 val (p,_,f, nxt,_,pt) = CalcTreeTEST [(fmz, refs)];
3.13 +val ptp = (pt, p);
3.14 +( *-------- outcomment EITHER above OR below --------------------------------------------------*)
3.15 +case get_example "Diff_App/No.123 a" of
3.16 + (_, ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" :: _,
3.17 + ("Diff_App", ["univariate_calculus", "Optimisation"] ,["Optimisation", "by_univariate_calculus"])))
3.18 + => ()
3.19 +| _ => error "intermed. example_store CHANGED";
3.20 +val p = ([], Pbl);
3.21 +val pt = update_state (*here we have Ctree.EmptyPtree and thus call init_ctree*)
3.22 +("Diff_App/No.123 a",
3.23 + (* Problem.parse_model_input results in markup, which is accepted by \<open>fun update_state\<close>, too:
3.24 + Constants [r = 7] *)
3.25 + ( [("#Given", ["Constants [r = 7]"]),
3.26 + ("#Where", ["0 < r"]),
3.27 + ("#Find", ["Maximum A", "AdditionalValues [u, v]"]),
3.28 + ("#Relate", ["Extremum A = 2 * u * v - u \<up> 2",
3.29 + "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]"])
3.30 + ],
3.31 + ("Diff_App", ["univariate_calculus", "Optimisation"], ["Optimisation", "by_univariate_calculus"])
3.32 + (*References_Def.explode_id ^^^^^^^^^^^^^^^^^^^^^^, ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
3.33 + )
3.34 +) Ctree.EmptyPtree;
3.35 +val ptp = (pt, p);
3.36 +(*\------- start example as required in VSCode_Example.thy -----------------------------------*)
3.37
3.38 (*** stepwise Specification: Problem model================================================= ***)
3.39 +(** ) we drop this step, because the user shall be presented a (empty) Model ... ( ** )
3.40 val ("ok", ([(Model_Problem, Model_Problem' (["univariate_calculus", "Optimisation"], _, _), _)], _, ptp))
3.41 - = Step.specify_do_next (pt, p);
3.42 -val ("ok", ([(Add_Given "Constants [r = 7]", _, _)], _, ptp))
3.43 = Step.specify_do_next ptp;
3.44 -val ("ok", ([(Add_Find "Maximum A", _, _)], _, ptp))
3.45 +( **)
3.46 +val ("ok", ([(Tactic.Add_Given "Constants [r = 7]", _, _)], _, ptp))
3.47 = Step.specify_do_next ptp;
3.48 -val ("ok", ([(Add_Find "AdditionalValues [u]", _, _)], _, ptp))
3.49 +val ("ok", ([(Tactic.Add_Find "Maximum A", _, _)], _, ptp))
3.50 = Step.specify_do_next ptp;
3.51 -val ("ok", ([(Add_Find "AdditionalValues [v]", _, _)], _, ptp))
3.52 +val ("ok", ([(Tactic.Add_Find "AdditionalValues [u]", _, _)], _, ptp))
3.53 = Step.specify_do_next ptp;
3.54 -val ("ok", ([(Add_Relation "Extremum (A = 2 * u * v - u \<up> 2)", _, _)], _, ptp))
3.55 +val ("ok", ([(Tactic.Add_Find "AdditionalValues [v]", _, _)], _, ptp))
3.56 = Step.specify_do_next ptp;
3.57 -val ("ok", ([(Add_Relation "SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]", _, _)], _, ptp))
3.58 +val ("ok", ([(Tactic.Add_Relation "Extremum (A = 2 * u * v - u \<up> 2)", _, _)], _, ptp))
3.59 + = Step.specify_do_next ptp;
3.60 +val ("ok", ([(Tactic.Add_Relation "SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]", _, _)], _, ptp))
3.61 = Step.specify_do_next ptp;
3.62
3.63 (*** Problem model is complete ============================================================ ***)
3.64 @@ -63,25 +91,44 @@
3.65 "(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]]))]"
3.66 then () else error "I_Model.to_string probl CHANGED";
3.67
3.68 -(*** Specification of References ========================================================== ***)
3.69 +(*//---------------- adhoc inserted ------------------------------------------------\\*)
3.70 +(*with update_state*)
3.71 +(* already been input -------vvvvvvvvvvvvvvvvvvv: code in check_input is missing*)
3.72 +(*+*)val ("ok", ([(Tactic.Add_Given "Constants [r = 7]", _, _)], _, ptp))
3.73 + = (**) Step.specify_do_next ptp;
3.74 +(*with update_state*)
3.75 +(*+*)val ("ERROR I_Model.check_single: \"Maximum A\"\" not for field \"#Find\"", ([], [], ptp))
3.76 + = (**) Step.specify_do_next ptp;
3.77 +(*\\---------------- adhoc inserted ------------------------------------------------//*)
3.78 +
3.79 +(*** Specification of References ========================================================== *** )
3.80 val ("ok", ([(Specify_Theory "Diff_App", _, _)], _, ptp))
3.81 = Step.specify_do_next ptp;
3.82 val ("ok", ([(Specify_Problem ["univariate_calculus", "Optimisation"], _, _)], _, ptp))
3.83 = Step.specify_do_next ptp;
3.84 val ("ok", ([(Specify_Method ["Optimisation", "by_univariate_calculus"], _, _)], _, ptp))
3.85 = Step.specify_do_next ptp;
3.86 +---------------------------------------------------------------------- trace from CalcTreeTEST*)
3.87
3.88 -(*** stepwise Specification: MethodC model ================================================ ***)
3.89 +(*** stepwise Specification: MethodC model ================================================ ***
3.90 +)
3.91 val ("ok", ([(Add_Given "FunctionVariable a", _, _)], _, ptp))
3.92 = Step.specify_do_next ptp;
3.93 val ("ok", ([(Add_Given "Input_Descript.Domain {0<..<r}", _, _)], _, ptp))
3.94 = Step.specify_do_next ptp;
3.95 val ("ok", ([(Add_Given "ErrorBound (\<epsilon> = 0)", _, _)], _, ptp))
3.96 = Step.specify_do_next ptp;
3.97 +---------------------------------------------------------------------- trace from CalcTreeTEST*)
3.98
3.99 (*** Specification of Problem and MethodC model is complete =============================== ***)
3.100 val PblObj {meth, ...} = get_obj I (fst ptp) [];
3.101 -if I_Model.to_string @{context} meth = "[\n" ^
3.102 +(*with update_state*)
3.103 +if I_Model.to_string @{context} meth = ("[\n" ^
3.104 + "(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] ,(fixes, [[r = 7]]))]"
3.105 +) then () else error "ERROR output CHANGED";
3.106 +
3.107 +(*with CalcTreeTEST* )
3.108 +if I_Model.to_string @ {context} meth = "[\n" ^
3.109 "(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] ,(fixes, [[r = 7]])), \n" ^
3.110 "(2 ,[1, 2, 3] ,true ,#Find ,Cor Maximum A ,(maxx, [A])), \n" ^
3.111 "(3 ,[1, 2, 3] ,true ,#Find ,Cor AdditionalValues [u, v] ,(vals, [[u, v]])), \n" ^
3.112 @@ -91,6 +138,7 @@
3.113 "(10 ,[1, 2] ,true ,#Given ,Cor Input_Descript.Domain {0<..<r} ,(doma, [{0<..<r}])), \n" ^
3.114 "(12 ,[1, 2, 3] ,true ,#Given ,Cor ErrorBound (\<epsilon> = 0) ,(err, [\<epsilon> = 0]))]"
3.115 then () else error "I_Model.to_string meth CHANGED";
3.116 +---------------------------------------------------------------------- trace from CalcTreeTEST*)
3.117
3.118 (*** Solution starts ====================================================================== ***)
3.119 (*---
4.1 --- a/test/Tools/isac/Test_Some.thy Tue Jul 26 22:11:41 2022 +0200
4.2 +++ b/test/Tools/isac/Test_Some.thy Tue Jul 26 22:29:35 2022 +0200
4.3 @@ -48,7 +48,7 @@
4.4 open Rewrite_Ord
4.5 open UnparseC
4.6 \<close>
4.7 -(**)ML_file "Specify/specify.sml"(**)
4.8 +(**)ML_file "BridgeJEdit/vscode-example.sml"(**)
4.9
4.10 section \<open>code for copy & paste ===============================================================\<close>
4.11 ML \<open>
4.12 @@ -108,156 +108,9 @@
4.13 \<close> ML \<open>
4.14 \<close>
4.15
4.16 -section \<open>====--- VSCode example with Step.specify_do_next ---===============================\<close>
4.17 +section \<open>===================================================================================\<close>
4.18 ML \<open>
4.19 \<close> ML \<open>
4.20 -(**** VSCode example with Step.specify_do_next ########################################### ****)
4.21 -"----------- VSCode example with Step.specify_do_next ------------------------------------------";
4.22 -"----------- VSCode example with Step.specify_do_next ------------------------------------------";
4.23 -val c = []:cid;
4.24 -val fmz = [
4.25 -(*Problem model:*)
4.26 - "Constants [r = (7::real)]", "Maximum A", "AdditionalValues [u, v]",
4.27 - "Extremum (A = 2 * u * v - u \<up> 2)",
4.28 - "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]",
4.29 - "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]",
4.30 - "SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]",
4.31 -(*MethodC model:*)
4.32 - "FunctionVariable a", "FunctionVariable b", "FunctionVariable \<alpha>",
4.33 - "Domain {0 <..< r}",
4.34 - "Domain {0 <..< r}",
4.35 - "Domain {0 <..< \<pi> / 2}",
4.36 - "ErrorBound (\<epsilon> = (0::real))"
4.37 -]: TermC.as_string list;
4.38 -if (fmz |> map (TermC.parseNEW @{context}) |> filter is_some |> length) = 14
4.39 -then () else error "Formalise.model not parsed completely";
4.40 -
4.41 -val refs =
4.42 -("Diff_App", ["univariate_calculus", "Optimisation"], ["Optimisation", "by_univariate_calculus"]);
4.43 -\<close> ML \<open>
4.44 -(*/------- start example as usual in tests ---------------------------------------------------* )
4.45 -val (p,_,f, nxt,_,pt) = CalcTreeTEST [(fmz, refs)];
4.46 -val ptp = (pt, p);
4.47 -( *-------- outcomment EITHER above OR below --------------------------------------------------*)
4.48 -case get_example "Diff_App/No.123 a" of
4.49 - (_, ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" :: _,
4.50 - ("Diff_App", ["univariate_calculus", "Optimisation"] ,["Optimisation", "by_univariate_calculus"])))
4.51 - => ()
4.52 -| _ => error "intermed. example_store CHANGED";
4.53 -val p = ([], Pbl);
4.54 -val pt = update_state (*here we have Ctree.EmptyPtree and thus call init_ctree*)
4.55 -("Diff_App/No.123 a",
4.56 - (* Problem.parse_model_input results in markup, which is accepted by \<open>fun update_state\<close>, too:
4.57 - Constants [r = 7] *)
4.58 - ( [("#Given", ["Constants [r = 7]"]),
4.59 - ("#Where", ["0 < r"]),
4.60 - ("#Find", ["Maximum A", "AdditionalValues [u, v]"]),
4.61 - ("#Relate", ["Extremum A = 2 * u * v - u \<up> 2",
4.62 - "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]"])
4.63 - ],
4.64 - ("Diff_App", ["univariate_calculus", "Optimisation"], ["Optimisation", "by_univariate_calculus"])
4.65 - (*References_Def.explode_id ^^^^^^^^^^^^^^^^^^^^^^, ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
4.66 - )
4.67 -) Ctree.EmptyPtree;
4.68 -val ptp = (pt, p);
4.69 -(*\------- start example as required in VSCode_Example.thy -----------------------------------*)
4.70 -
4.71 -\<close> ML \<open>
4.72 -(*** stepwise Specification: Problem model================================================= ***)
4.73 -(** ) we drop this step, because the user shall be presented a (empty) Model ... ( ** )
4.74 -val ("ok", ([(Model_Problem, Model_Problem' (["univariate_calculus", "Optimisation"], _, _), _)], _, ptp))
4.75 - = Step.specify_do_next ptp;
4.76 -( **)
4.77 -val ("ok", ([(Add_Given "Constants [r = 7]", _, _)], _, ptp))
4.78 - = Step.specify_do_next ptp;
4.79 -val ("ok", ([(Add_Find "Maximum A", _, _)], _, ptp))
4.80 - = Step.specify_do_next ptp;
4.81 -val ("ok", ([(Add_Find "AdditionalValues [u]", _, _)], _, ptp))
4.82 - = Step.specify_do_next ptp;
4.83 -val ("ok", ([(Add_Find "AdditionalValues [v]", _, _)], _, ptp))
4.84 - = Step.specify_do_next ptp;
4.85 -val ("ok", ([(Add_Relation "Extremum (A = 2 * u * v - u \<up> 2)", _, _)], _, ptp))
4.86 - = Step.specify_do_next ptp;
4.87 -val ("ok", ([(Add_Relation "SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]", _, _)], _, ptp))
4.88 - = Step.specify_do_next ptp;
4.89 -
4.90 -(*** Problem model is complete ============================================================ ***)
4.91 -val PblObj {probl, ...} = get_obj I (fst ptp) [];
4.92 -if I_Model.to_string @{context} probl = "[\n" ^
4.93 - "(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] ,(fixes, [[r = 7]])), \n" ^
4.94 - "(2 ,[1, 2, 3] ,true ,#Find ,Cor Maximum A ,(maxx, [A])), \n" ^
4.95 - "(3 ,[1, 2, 3] ,true ,#Find ,Cor AdditionalValues [u, v] ,(vals, [[u, v]])), \n" ^
4.96 - "(4 ,[1, 2, 3] ,true ,#Relate ,Cor Extremum (A = 2 * u * v - u \<up> 2) ,(extr, [A = 2 * u * v - u \<up> 2])), \n" ^
4.97 - "(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]]))]"
4.98 -then () else error "I_Model.to_string probl CHANGED";
4.99 -
4.100 -\<close> ML \<open> (*//---------------- adhoc inserted ------------------------------------------------\\*)
4.101 -\<close> ML \<open> (*with update_state*)
4.102 -(* already been input -------vvvvvvvvvvvvvvvvvvv: code in check_input is missing*)
4.103 -(*+*)val ("ok", ([(Add_Given "Constants [r = 7]", _, _)], _, ptp))
4.104 - = (**) Step.specify_do_next ptp;
4.105 -\<close> ML \<open> (*with update_state*)
4.106 -(*+*)val ("ERROR I_Model.check_single: \"Maximum A\"\" not for field \"#Find\"", ([], [], ptp))
4.107 - = (**) Step.specify_do_next ptp;
4.108 -\<close> ML \<open>
4.109 -\<close> text \<open> (*\\---------------- adhoc inserted ------------------------------------------------//*)
4.110 -(*** Specification of References ========================================================== ***)
4.111 -val ("ok", ([(Specify_Theory "Diff_App", _, _)], _, ptp))
4.112 - = Step.specify_do_next ptp;
4.113 -val ("ok", ([(Specify_Problem ["univariate_calculus", "Optimisation"], _, _)], _, ptp))
4.114 - = Step.specify_do_next ptp;
4.115 -val ("ok", ([(Specify_Method ["Optimisation", "by_univariate_calculus"], _, _)], _, ptp))
4.116 - = Step.specify_do_next ptp;
4.117 -\<close> text \<open>
4.118 -
4.119 -(*** stepwise Specification: MethodC model ================================================ ***)
4.120 -val ("ok", ([(Add_Given "FunctionVariable a", _, _)], _, ptp))
4.121 - = Step.specify_do_next ptp;
4.122 -val ("ok", ([(Add_Given "Input_Descript.Domain {0<..<r}", _, _)], _, ptp))
4.123 - = Step.specify_do_next ptp;
4.124 -val ("ok", ([(Add_Given "ErrorBound (\<epsilon> = 0)", _, _)], _, ptp))
4.125 - = Step.specify_do_next ptp;
4.126 -
4.127 -(*** Specification of Problem and MethodC model is complete =============================== ***)
4.128 -\<close> ML \<open>
4.129 -val PblObj {meth, ...} = get_obj I (fst ptp) [];
4.130 -\<close> ML \<open>
4.131 -(*+*)I_Model.to_string @{context} meth
4.132 -\<close> text \<open> (*with update_state*)
4.133 -if I_Model.to_string @ {context} meth = ("[\n" ^
4.134 - "(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L ,(l_l, [L])), \n" ^
4.135 - "(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^
4.136 - "(3 ,[1] ,true ,#Find ,Cor Biegelinie y ,(b_b, [y])), \n" ^
4.137 - "(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" ^
4.138 - "(5 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(fun_var, [x])), \n" ^
4.139 ------- these are from Biegelinie: utterly wrong.
4.140 - "(6 ,[1] ,true ,#Given ,Cor GleichungsVariablen [c, c_2, c_3, c_4] ,(vs, [[c, c_2, c_3, c_4]])), \n" ^
4.141 - "(7 ,[1] ,true ,#Given ,Cor AbleitungBiegelinie dy ,(id_der, [dy]))]")
4.142 -then () else error "";
4.143 -\<close> ML \<open>
4.144 -\<close> text \<open> (*with *)
4.145 -if I_Model.to_string @ {context} meth = "[\n" ^
4.146 - "(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] ,(fixes, [[r = 7]])), \n" ^
4.147 - "(2 ,[1, 2, 3] ,true ,#Find ,Cor Maximum A ,(maxx, [A])), \n" ^
4.148 - "(3 ,[1, 2, 3] ,true ,#Find ,Cor AdditionalValues [u, v] ,(vals, [[u, v]])), \n" ^
4.149 - "(4 ,[1, 2, 3] ,true ,#Relate ,Cor Extremum (A = 2 * u * v - u \<up> 2) ,(extr, [A = 2 * u * v - u \<up> 2])), \n" ^
4.150 - "(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" ^
4.151 - "(7 ,[1] ,true ,#Given ,Cor FunctionVariable a ,(funvar, [a])), \n" ^
4.152 - "(10 ,[1, 2] ,true ,#Given ,Cor Input_Descript.Domain {0<..<r} ,(doma, [{0<..<r}])), \n" ^
4.153 - "(12 ,[1, 2, 3] ,true ,#Given ,Cor ErrorBound (\<epsilon> = 0) ,(err, [\<epsilon> = 0]))]"
4.154 -then () else error "I_Model.to_string meth CHANGED";
4.155 -
4.156 -(*** Solution starts ====================================================================== ***)
4.157 -(*---
4.158 -Step.specify_do_next ptp;
4.159 -(*ERinROR in creating the environment from formal args. of partial_function "Diff_App.univar_optimisation"
4.160 -and the actual args., ie. items of the guard of "["Optimisation", "by_univariate_calculus"]" by "assoc_by_type":
4.161 -formal arg "err" of type "bool" doesn't mach an actual arg.
4.162 -with:
4.163 -7 formal args: ["fixes", "maxx", "extr", "sideconds", "funvar", "doma", "err"]
4.164 -7 actual args: ["[r = 7]", "A", "[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]", "a", "{0<..<r}", "\<epsilon> = 0", "[u, v]"]
4.165 - with types: ["bool list", "real", "bool list", "real", "real set", "bool", "real list"]*)
4.166 ----*)
4.167 \<close> ML \<open>
4.168 \<close> ML \<open>
4.169 \<close>