1.1 --- a/src/Tools/isac/BridgeJEdit/Calculation.thy Thu Jun 02 17:53:41 2022 +0200
1.2 +++ b/src/Tools/isac/BridgeJEdit/Calculation.thy Fri Jun 17 12:15:09 2022 +0200
1.3 @@ -37,22 +37,51 @@
1.4 );
1.5
1.6 val set_data = Data.put o SOME;
1.7 -val the_data = the o Data.get;
1.8 +fun the_data thy =
1.9 + case Data.get thy of NONE => Ctree.EmptyPtree
1.10 + | SOME ctree => ctree;
1.11 +\<close> ML \<open>
1.12 +\<close> text \<open>
1.13 +A provisional Example collection.
1.14
1.15 +For notes from ISAC's discontinued Java front-end see
1.16 +https://isac.miraheze.org/wiki/Extend_ISAC_Knowledge#Add_an_example_in_XML_format
1.17 \<close> ML \<open>
1.18 +type description = string
1.19 +type example = (description * Formalise.T)
1.20 +val example_store = []: (string * example) list
1.21 \<close> ML \<open>
1.22 -val specify_data_empty =
1.23 - {fmz = Formalise.empty, origin = (O_Model.empty, References.empty, TermC.empty),
1.24 - spec = References.empty, probl = []: Model_Def.i_model, meth = []: Model_Def.i_model,
1.25 - ctxt = ContextC.empty, loc = (NONE, NONE),
1.26 - branch = Ctree.NoBranch, ostate = Ctree.Incomplete, result = (TermC.empty, [])}: Ctree.specify_data
1.27 -;
1.28 -Ctree.Nd (Ctree.PblObj specify_data_empty, []): Ctree.ctree
1.29 +val example_store = AList.update op= ("Diff_App/No.123 a",
1.30 + ("The efficiency of an electrical coil depends on the mass of the kernel." ^
1.31 + "Given is a kernel with cross-sectional area determined by two rectangles" ^
1.32 + "of same shape as shown in the figure." ^
1.33 + "Given a radius r = 7, determine the length u and width v of the rectangles" ^
1.34 + "such that the cross-sectional area A (and thus the mass of the kernel) is a" ^
1.35 + "maximum. + Figure",
1.36 + (["[r = 7]", "[A, [u, v]]", "[A = 2 \<sqdot> u \<sqdot> v - u 2 , ( 2 u ) 2 + ( 2 v ) 2 = r 2 ]",
1.37 + "{0 < .. < r}"]: TermC.as_string list,
1.38 + (*TODO: compare paper + test/../DiffApp: more than one list of Model_Def.form_model? *)
1.39 + ("Diff_App", ["univariate_calculus", "Optimisation"],
1.40 + ["Optimisation", "by_univariate_calculus"]): References.T)): example) example_store
1.41 +\<close> ML \<open>
1.42 +case AList.lookup op= example_store "Diff_App/No.123 a" of
1.43 + SOME (_, (["[r = 7]", "[A, [u, v]]", "[A = 2 \<sqdot> u \<sqdot> v - u 2 , ( 2 u ) 2 + ( 2 v ) 2 = r 2 ]", "{0 < .. < r}"],
1.44 + ("Diff_App", ["univariate_calculus", "Optimisation"] ,["Optimisation", "by_univariate_calculus"])))
1.45 + => ()
1.46 +| _ => error "intermed. example_store CHANGED";
1.47 +\<close> ML \<open>
1.48 \<close> ML \<open>
1.49 (*? I_Model.* or Problem.* ?*)
1.50 fun check_input (*ctxt o-model ??*) (_: Problem.model_input) = []: I_Model.T
1.51 \<close> ML \<open>
1.52 -fun update_state (model, (thy_id, probl_id, meth_id)) (*TODO +switch RProblem | RMethod*)
1.53 +fun update_state (model, (thy_id, probl_id, meth_id)) (*at the first encounter of an Example*)
1.54 + Ctree.EmptyPtree =
1.55 + Ctree.Nd (Ctree.PblObj {
1.56 + fmz = Formalise.empty, origin = (O_Model.empty, References.empty, TermC.empty),
1.57 + spec = (thy_id, probl_id, meth_id), probl = check_input model, meth = []: Model_Def.i_model,
1.58 + ctxt = ContextC.empty, loc = (NONE, NONE),
1.59 + branch = Ctree.NoBranch, ostate = Ctree.Incomplete, result = (TermC.empty, [])}, [])
1.60 + | update_state (model, (thy_id, probl_id, meth_id)) (*TODO +switch RProblem | RMethod*)
1.61 (Ctree.Nd (Ctree.PblObj {fmz, origin, spec = _, probl = _, meth, ctxt, loc, branch, ostate, result},
1.62 children)) =
1.63 Ctree.Nd (Ctree.PblObj {
1.64 @@ -60,13 +89,6 @@
1.65 spec = (thy_id, probl_id, meth_id), probl = check_input model, meth = meth,
1.66 ctxt = ctxt, loc = loc,
1.67 branch = branch, ostate = ostate, result = result}, children)
1.68 - | update_state (model, (thy_id, probl_id, meth_id)) (*TODO +switch RProblem | RMethod*)
1.69 - Ctree.EmptyPtree =
1.70 - Ctree.Nd (Ctree.PblObj {
1.71 - fmz = Formalise.empty, origin = (O_Model.empty, References.empty, TermC.empty),
1.72 - spec = (thy_id, probl_id, meth_id), probl = check_input model, meth = []: Model_Def.i_model,
1.73 - ctxt = ContextC.empty, loc = (NONE, NONE),
1.74 - branch = Ctree.NoBranch, ostate = Ctree.Incomplete, result = (TermC.empty, [])}, [])
1.75 | update_state _ _ = raise ERROR "update_state: uncovered case in fun.def."
1.76 \<close> ML \<open>
1.77 update_state: Problem.model_input * (ThyC.id * Problem.id * MethodC.id)
1.78 @@ -79,15 +101,14 @@
1.79 Parse.!!! ( \<^keyword>\<open>Problem_Ref\<close> -- \<^keyword>\<open>Theory_Ref\<close> |-- Parse.name --
1.80 Parse.!!! ( \<^keyword>\<open>Method_Ref\<close> -- \<^keyword>\<open>Theory_Ref\<close> |-- Parse.name)))
1.81 \<close> ML \<open>
1.82 -parse_references_input: references_input parser
1.83 -\<close> ML \<open>
1.84 +parse_references_input: references_input parser (*TODO: dpes not yet work,
1.85 + thus in Outer_Syntax.command \<^command_keyword>\<open>Example\<close> replacced by Problem.parse_cas*)
1.86 \<close> ML \<open>
1.87 op -- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e;
1.88 op |-- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'd * 'e
1.89 \<close> ML \<open>
1.90 \<close> ML \<open>
1.91 \<close> ML \<open>
1.92 -
1.93 val _ =
1.94 Outer_Syntax.command \<^command_keyword>\<open>Example\<close>
1.95 "prepare ISAC problem type and register it to Knowledge Store"