1.1 --- a/src/Tools/isac/BridgeJEdit/Calculation.thy Mon Feb 13 15:37:41 2023 +0100
1.2 +++ b/src/Tools/isac/BridgeJEdit/Calculation.thy Mon Feb 13 15:50:53 2023 +0100
1.3 @@ -26,7 +26,7 @@
1.4
1.5 ML \<open>
1.6 \<close> ML \<open>
1.7 -\<close> ML \<open>
1.8 +\<close> ML \<open> (** intermed. example_store **)
1.9 structure Data = Theory_Data
1.10 (
1.11 type T = Ctree.ctree option;
1.12 @@ -76,7 +76,7 @@
1.13 => ()
1.14 | _ => error "intermed. example_store CHANGED";
1.15 \<close> ML \<open>
1.16 -\<close> ML \<open>
1.17 +\<close> ML \<open> (** check_input **)
1.18 (*
1.19 Implementation reasonable, as soo as
1.20 * clarified, how "empty" items in Model are represented
1.21 @@ -84,17 +84,16 @@
1.22 * switching \<Odot>\<Otimes> i_model for probl and meth works.
1.23 *)
1.24 \<close> ML \<open>
1.25 -val check_inputXXX = I_Model.complete (*in order *)
1.26 +val check_inputXXX = I_Model.complete (*in order xxx*)
1.27 \<close> ML \<open>
1.28 fun check_input (*ctxt o-model ??*) (_: Problem.model_input_pos) = []: I_Model.T (*TODO*)
1.29 \<close> ML \<open>
1.30 -\<close> ML \<open>
1.31 +\<close> ML \<open> (** init or update state **)
1.32 (* at the first encounter of an Example create the following data and transfer them to ctree:
1.33 origin: eventually used by sub-problems, too
1.34 O_Model: for check of missing items
1.35 I_Model: for efficient check of user input
1.36 *)
1.37 -\<close> ML \<open>
1.38 fun init_ctree example_id =
1.39 let
1.40 val thy = ThyC.get_theory @{context} "Diff_App"
1.41 @@ -136,7 +135,7 @@
1.42 ;
1.43 update_state: string * (Problem.model_input_pos * References.input) -> Ctree.ctree -> Ctree.ctree
1.44 \<close> ML \<open>
1.45 -(* the first indication for a user model *)
1.46 +\<close> ML \<open> (** first indication for a user model **)
1.47 datatype user_model_spec = Model_Refs | Model | None
1.48 val user_model_spec = Model_Refs
1.49 \<close> ML \<open>
1.50 @@ -152,6 +151,7 @@
1.51 show_template: user_model_spec ->
1.52 (P_Model.switch_pbl_met * P_Model.model_out) * References.input -> string
1.53 \<close> ML \<open>
1.54 +\<close> ML \<open> (** Outer_Syntax.command **)
1.55 val _ =
1.56 Outer_Syntax.command \<^command_keyword>\<open>Example\<close>
1.57 "prepare ISAC problem type and register it to Knowledge Store"
2.1 --- a/src/Tools/isac/BridgeJEdit/VSCode_Example.thy Mon Feb 13 15:37:41 2023 +0100
2.2 +++ b/src/Tools/isac/BridgeJEdit/VSCode_Example.thy Mon Feb 13 15:50:53 2023 +0100
2.3 @@ -53,7 +53,7 @@
2.4 Find: \<open>Maximum A\<close> \<open>AdditionalValues u, v\<close>
2.5 Relate: \<open>Extremum A = 2 \<sqdot> u \<sqdot> v − u \<up> 2\<close> \<open>SideCondition (u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2\<close>
2.6 References:
2.7 - Theory_Ref: "Diff_App"
2.8 + Theory_Ref: "Diff_App"
2.9 (*\<Otimes>*) Problem_Ref: "univariate_calculus/Optimisation"
2.10 (*\<Odot>*) Method_Ref: "Optimisation/by_univariate_calculus"
2.11 (*Solution:*)
2.12 @@ -71,10 +71,11 @@
2.13 Where: \<open>0 < r\<close>
2.14 Find: \<open>Maximum _\<close> \<open>AdditionalValues _\<close>
2.15 Relate: \<open>Extremum _\<close> \<open>SideCondition _\<close> References:
2.16 - Theory_Ref: "_"
2.17 - \<Otimes> Problem_Ref: "_/_"
2.18 - \<Odot> Method_Ref: "_/_"
2.19 - Solution:
2.20 + References:
2.21 + Theory_Ref: "Diff_App"
2.22 + (*\<Otimes>*) Problem_Ref: "univariate_calculus/Optimisation"
2.23 + (*\<Odot>*) Method_Ref: "Optimisation/by_univariate_calculus"
2.24 +(*Solution:*)
2.25
2.26 (* remove as soon as this ^^^ works as Isabelle/Isar commands ..*) \<close>
2.27
2.28 @@ -149,11 +150,11 @@
2.29 Where:
2.30 Find: \<open>extrema\<close>
2.31 Relate:
2.32 - References:
2.33 - Theory_Ref: "Diff_App"
2.34 - \<Odot> Problem_Ref: "univariate_calculus/Optimisation"
2.35 - \<Otimes> Method_Ref: "Optimisation/by_univariate_calculus"
2.36 - Solution:
2.37 + References:
2.38 + Theory_Ref: "Diff_App"
2.39 + (*\<Otimes>*) Problem_Ref: "univariate_calculus/Optimisation"
2.40 + (*\<Odot>*) Method_Ref: "Optimisation/by_univariate_calculus"
2.41 +(*Solution:*)
2.42
2.43 (* remove as soon as this ^^^ works as Isabelle/Isar commands ..*) \<close>
2.44
2.45 @@ -228,9 +229,10 @@
2.46 Relate: \<open>Extremum A = 2 * u * v - u \<up> 2\<close>
2.47 \<open>SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]\<close>
2.48 References:
2.49 - Theory_Ref: "Diff_App"
2.50 - (*\<Odot>*) Problem_Ref: "univariate_calculus/Optimisation"
2.51 - (*\<Otimes>*) Method_Ref: "Optimisation/by_univariate_calculus"
2.52 + Theory_Ref: "Diff_App"
2.53 + (*\<Otimes>*) Problem_Ref: "univariate_calculus/Optimisation"
2.54 + (*\<Odot>*) Method_Ref: "Optimisation/by_univariate_calculus"
2.55 +(*Solution:*)
2.56
2.57 ML \<open>
2.58 val state = the_data @{theory}; (* state filled from the above Example by \<open>fun update_state\<close> *)
3.1 --- a/src/Tools/isac/Specify/p-model.sml Mon Feb 13 15:37:41 2023 +0100
3.2 +++ b/src/Tools/isac/Specify/p-model.sml Mon Feb 13 15:50:53 2023 +0100
3.3 @@ -2,7 +2,7 @@
3.4 Author: Walther Neuper 170207
3.5 (c) due to copyright terms
3.6
3.7 -This will be dropped at switch to Isabelle/PIDE .
3.8 +This will mostly be dropped at switch to Isabelle/PIDE .
3.9 *)
3.10
3.11 signature PRESENTATION_MODEL =
3.12 @@ -96,7 +96,7 @@
3.13 in (given, where_, find, relate) end
3.14
3.15 fun template_args switch_pbl_met input_refs store =
3.16 - if not (Ctree.is_pblnd store) then raise ERROR "update code w.r.t. to future design of Solution"
3.17 + if not (Ctree.is_pblnd store) then raise ERROR "extend code w.r.t. to future design of Solution"
3.18 else
3.19 let
3.20 val Ctree.Nd (Ctree.PblObj {origin = (_, o_refs, _), probl, meth, spec, ctxt, ...}, []) = store
4.1 --- a/test/Pure/Isar/README Mon Feb 13 15:37:41 2023 +0100
4.2 +++ b/test/Pure/Isar/README Mon Feb 13 15:50:53 2023 +0100
4.3 @@ -3,24 +3,20 @@
4.4 these files will be cleaned up.
4.5
4.6 ~~$ ls -l test/Pure/Isar/
4.7 -DEL Check_Outer_Syntax.thy Survey on checked examples
4.8 +Check_Outer_Syntax.thy Survey on checked examples
4.9 Decompose examples: ISAC :: diag, forthel :: thy_decl, spark_status :: diag
4.10 Outer_Syntax.command..spark_open_vcg :: thy_load
4.11 -DEL Downto_Synchorinzed.thy trace code down to storage of a proof
4.12 -MIS Keyword_ISAC.thy original from Makarius 2018
4.13 -MIS Test_Parse_Isac.thy definitions for keywords
4.14 +Downto_Synchorinzed.thy trace code down to storage of a proof
4.15 +Keyword_ISAC.thy original from Makarius 2018
4.16 +Test_Parse_Isac.thy definitions for keywords
4.17 ^^^^^^^^^^^^^^^^^^^| Tools and Goals
4.18 | Stepwise extending parser: Problem headline .. Problem
4.19 +----> cp --> ~~/src/Tools/isac/BridgeJEdit/parseC.sml
4.20 Test_Parsers.thy scanner combinators from src/Pure/General/scan.ML
4.21 parse compound suffixes: Lists, terms, -- Scan.optional, ...
4.22 -MIS Test_Parse_Term.thy parse following Stefan Berghofer at Isabelle Developer Workshop 2010
4.23 +Test_Parse_Term.thy parse following Stefan Berghofer at Isabelle Developer Workshop 2010
4.24 decompose term
4.25 Test_Parsers_Cookbook.thy Work along book: Scan strings, Scan token list, Scan.optional,
4.26 recursive parsers
4.27 -MIS Theory_Commands.thy original from Makarius 2020 + Isac example
4.28 +Theory_Commands.thy original from Makarius 2020 + Isac example
4.29 ^^^^^^^^^^^^^^^^^^^<----- ML_file "~~/src/Tools/isac/BridgeJEdit/parseC.sml"
4.30 -
4.31 -Legend 230213
4.32 -DEL deleted before starting "PIDE turn 0"
4.33 -MIS missing on 230213
4.34 \ No newline at end of file
5.1 --- a/test/Tools/isac/BridgeJEdit/Test_VSCode_Example.thy Mon Feb 13 15:37:41 2023 +0100
5.2 +++ b/test/Tools/isac/BridgeJEdit/Test_VSCode_Example.thy Mon Feb 13 15:50:53 2023 +0100
5.3 @@ -1,12 +1,49 @@
5.4 theory Test_VSCode_Example
5.5 - imports "Isac.Calculation"
5.6 + imports "Isac.Build_Isac" (*"Isac.Calculation"*)
5.7 + keywords "Test_Example" :: thy_decl
5.8 begin
5.9
5.10 +text \<open>
5.11 + Tests here in BridgePIDE are already based on Build_Isac.thy bypassing $ISABELLE_ISAC_TEST.
5.12 + TODO: eliminate "Isac." above on eliminating session in $ISABELLE_ISAC_TEST.
5.13 +\<close>
5.14 +
5.15 +subsection \<open>Development\<close>
5.16 +text \<open>
5.17 + Here we develop the semantics of \<open>Example\<close> intermediately within one single theory
5.18 + for \<open>Test_Example\<close> before we transfer the development to production code in src/* .
5.19 +\<close> ML \<open>
5.20 +\<close> ML \<open> (** Outer_Syntax.command **)
5.21 +(*cp from src/../Calculation.thy just for start*)
5.22 +val _ =
5.23 + Outer_Syntax.command \<^command_keyword>\<open>Test_Example\<close>
5.24 + "prepare ISAC problem type and register it to Knowledge Store"
5.25 + (Parse.name -- Parse.!!! ( \<^keyword>\<open>Specification\<close> -- \<^keyword>\<open>:\<close> --
5.26 + \<^keyword>\<open>Model\<close> -- \<^keyword>\<open>:\<close> |-- Problem.parse_pos_model_input --
5.27 + (\<^keyword>\<open>References\<close> -- \<^keyword>\<open>:\<close> |-- Parse.!!! References.parse_input_pos
5.28 + (** )-- ( \<^keyword>\<open>Solution\<close> -- keyword>\<open>:\<close>)( ** )WHAT IS WRONG HEREWITH?( **)) ) >>
5.29 + (fn (example_id, (model_input,
5.30 + ((thy_id, thy_id_pos), ((probl_id, probl_id_pos), (meth_id, meth_id_pos))))) =>
5.31 + Toplevel.theory (fn thy =>
5.32 + let
5.33 + val store = update_state (example_id, (model_input, (thy_id, probl_id, meth_id)))
5.34 + Ctree.EmptyPtree;
5.35 + (*---vvvvvvvvvvvvvv------- this comes from input \<Otimes> \<Odot> to Example *)
5.36 + val (switch_pbl_met, user_model_spec) = (P_Model.Model_For_Problem_Ref, Model_Refs)
5.37 + val args = P_Model.template_args switch_pbl_met (thy_id, probl_id, meth_id) store
5.38 + val _ = show_template user_model_spec args
5.39 + in set_data store thy end)));
5.40 +\<close> ML \<open>
5.41 +\<close>
5.42 +
5.43 subsubsection \<open>Complete Specification at once\<close>
5.44 text \<open>
5.45 Just a test, that this works also in $ISABELLE_ISAC_TEST
5.46 \<close>
5.47
5.48 +text \<open>
5.49 + Check complete \<open>Model\<close>, infer empty \<open>References\<close> from data hidden in "Diff_App-No.123a"
5.50 +\<close>
5.51 Example "Diff_App-No.123a"
5.52 Specification:
5.53 Model:
5.54 @@ -21,7 +58,7 @@
5.55 (*\<Otimes>*) Method_Ref: "Optimisation/by_univariate_calculus"
5.56 (*Solution:*)
5.57
5.58 -subsubsection \<open>Empty Specification to be input by students\<close>
5.59 +subsubsection \<open>Empty Specification ready for input by students\<close>
5.60 text \<open>
5.61 In order to help the student (similar to a personal instructur helping a beginner)
5.62 the \<open>Specification\<close> is given as a template,
5.63 @@ -29,7 +66,7 @@
5.64 (in native language!) and delimiters are (partially) given.
5.65
5.66 For the same reason \<open>Where\<close> is already filled; most beginners are
5.67 - not aware of "where_-conditions".
5.68 + not aware of "where_-conditions", i.e. of preconditions.
5.69 \<close>
5.70
5.71 Example "Diff_App-No.123a" (* FIXME template *)
5.72 @@ -41,7 +78,7 @@
5.73 Relate: \<open>Extremum __\<close>
5.74 \<open>SideConditions [__]\<close>
5.75 References:
5.76 - Theory_Ref: "__"
5.77 + Theory_Ref: "__"
5.78 (*\<Odot>*) Problem_Ref: "__/__"
5.79 (*\<Otimes>*) Method_Ref: "__/__"
5.80 (*Solution:*)
5.81 @@ -147,9 +184,9 @@
5.82 Relate: \<open>Extremum __\<close>
5.83 \<open>SideConditions [__]\<close>
5.84 References:
5.85 - Theory_Ref: "__"
5.86 - (*\<Odot>*) Problem_Ref: "__/__"
5.87 - (*\<Otimes>*) Method_Ref: "__/__"
5.88 + Theory_Ref: "__"
5.89 + (*\<Odot>*) Problem_Ref: "__/__"
5.90 + (*\<Otimes>*) Method_Ref: "__/__"
5.91 (*Solution:*)
5.92
5.93 text \<open>
5.94 @@ -169,9 +206,9 @@
5.95 Find: \<open>Maximum _\<close> \<open>AdditionalValues [_]\<close>
5.96 Relate: \<open>Extremum _\<close> \<open>SideConditions [_]\<close>
5.97 References:
5.98 - Theory_Ref: "__"
5.99 - (*\<Odot>*) Problem_Ref: "__/__"
5.100 - (*\<Otimes>*) Method_Ref: "__/__"
5.101 + Theory_Ref: "__"
5.102 + (*\<Odot>*) Problem_Ref: "__/__"
5.103 + (*\<Otimes>*) Method_Ref: "__/__"
5.104 (*Solution:*)
5.105
5.106 text \<open>
5.107 @@ -190,9 +227,9 @@
5.108 Find: \<open>Maximum _\<close> \<open>AdditionalValues [u]\<close>
5.109 Relate: \<open>Extremum _\<close> \<open>SideConditions [_]\<close>
5.110 References:
5.111 - Theory_Ref: "__"
5.112 - (*\<Odot>*) Problem_Ref: "__/__"
5.113 - (*\<Otimes>*) Method_Ref: "__/__"
5.114 + Theory_Ref: "__"
5.115 + (*\<Odot>*) Problem_Ref: "__/__"
5.116 + (*\<Otimes>*) Method_Ref: "__/__"
5.117 (*Solution:*)
5.118
5.119 text \<open>
5.120 @@ -211,9 +248,9 @@
5.121 Find: \<open>Maximum _\<close> \<open>AdditionalValues [u, v]\<close>
5.122 Relate: \<open>Extremum _\<close> \<open>SideConditions [_]\<close>
5.123 References:
5.124 - Theory_Ref: "__"
5.125 - (*\<Odot>*) Problem_Ref: "__/__"
5.126 - (*\<Otimes>*) Method_Ref: "__/__"
5.127 + Theory_Ref: "__"
5.128 + (*\<Odot>*) Problem_Ref: "__/__"
5.129 + (*\<Otimes>*) Method_Ref: "__/__"
5.130 (*Solution:*)
5.131
5.132 text \<open>
5.133 @@ -229,9 +266,9 @@
5.134 Find: \<open>Maximum _\<close> \<open>AdditionalValues [u, v]\<close>
5.135 Relate: \<open>Extremum _\<close> \<open>SideConditions [_]\<close>
5.136 References:
5.137 - Theory_Ref: "__"
5.138 - (*\<Odot>*) Problem_Ref: "__/__"
5.139 - (*\<Otimes>*) Method_Ref: "__/__"
5.140 + Theory_Ref: "__"
5.141 + (*\<Odot>*) Problem_Ref: "__/__"
5.142 + (*\<Otimes>*) Method_Ref: "__/__"
5.143 (*Solution:*)
5.144
5.145 text \<open>
5.146 @@ -249,7 +286,7 @@
5.147 Find: \<open>Maximum _\<close> \<open>AdditionalValues [u, v]\<close>
5.148 Relate: \<open>Extremum _\<close> \<open>SideConditions [_]\<close>
5.149 References:
5.150 - Theory_Ref: "__"
5.151 + Theory_Ref: "__"
5.152 (*\<Odot>*) Problem_Ref: "univariate_calculus/Optimisation"
5.153 (*\<Otimes>*) Method_Ref: "Optimisation/by_univariate_calculus"
5.154 (*Solution:*)