1.1 --- a/src/Tools/isac/BridgeJEdit/Calculation.thy Mon Jun 20 09:56:48 2022 +0200
1.2 +++ b/src/Tools/isac/BridgeJEdit/Calculation.thy Mon Jun 20 11:51:12 2022 +0200
1.3 @@ -49,39 +49,76 @@
1.4 \<close> ML \<open>
1.5 type description = string
1.6 type example = (description * Formalise.T)
1.7 -val example_store = []: (string * example) list
1.8 +type example_id = string
1.9 +val example_store = Unsynchronized.ref ([]: (example_id * example) list)
1.10 +fun get_example example_id =
1.11 + case AList.lookup op= (!example_store) example_id of
1.12 + NONE => raise ERROR ("Examnple " ^ quote example_id ^ " not found")
1.13 + | SOME expl => expl
1.14 \<close> ML \<open>
1.15 -val example_store = AList.update op= ("Diff_App/No.123 a",
1.16 +get_example: example_id -> example;
1.17 +\<close> ML \<open>
1.18 +example_store := AList.update op= ("Diff_App/No.123 a",
1.19 ("The efficiency of an electrical coil depends on the mass of the kernel." ^
1.20 "Given is a kernel with cross-sectional area determined by two rectangles" ^
1.21 "of same shape as shown in the figure." ^
1.22 "Given a radius r = 7, determine the length u and width v of the rectangles" ^
1.23 "such that the cross-sectional area A (and thus the mass of the kernel) is a" ^
1.24 "maximum. + Figure",
1.25 - (["[r = 7]", "[A, [u, v]]", "[A = 2 \<sqdot> u \<sqdot> v - u 2 , ( 2 u ) 2 + ( 2 v ) 2 = r 2 ]",
1.26 - "{0 < .. < r}"]: TermC.as_string list,
1.27 - (*TODO: compare paper + test/../Diff_App: more than one list of Model_Def.form_model? *)
1.28 + ([
1.29 + (*Problem model:*)
1.30 + "Constants [r = (7::real)]", "Maximum A", "AdditionalValues [u, v]",
1.31 + "Extremum (A = 2 * u * v - u \<up> 2)",
1.32 + "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]",
1.33 + "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]",
1.34 + "SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]",
1.35 + (*MethodC model:*)
1.36 + "FunctionVariable a", "FunctionVariable b", "FunctionVariable \<alpha>",
1.37 + "Domain {0 <..< r}",
1.38 + "Domain {0 <..< r}",
1.39 + "Domain {0 <..< \<pi> / 2}",
1.40 + "ErrorBound (\<epsilon> = (0::real))"]: TermC.as_string list,
1.41 ("Diff_App", ["univariate_calculus", "Optimisation"],
1.42 - ["Optimisation", "by_univariate_calculus"]): References.T)): example) example_store
1.43 + ["Optimisation", "by_univariate_calculus"]): References.T)): example) (!example_store)
1.44 \<close> ML \<open>
1.45 -case AList.lookup op= example_store "Diff_App/No.123 a" of
1.46 - 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.47 +case get_example "Diff_App/No.123 a" of
1.48 + (_, ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" :: _,
1.49 ("Diff_App", ["univariate_calculus", "Optimisation"] ,["Optimisation", "by_univariate_calculus"])))
1.50 => ()
1.51 | _ => error "intermed. example_store CHANGED";
1.52 \<close> ML \<open>
1.53 \<close> ML \<open>
1.54 -(*? I_Model.* or Problem.* ?*)
1.55 fun check_input (*ctxt o-model ??*) (_: Problem.model_input) = []: I_Model.T
1.56 \<close> ML \<open>
1.57 -fun update_state (model, (thy_id, probl_id, meth_id)) (*at the first encounter of an Example*)
1.58 - Ctree.EmptyPtree =
1.59 - Ctree.Nd (Ctree.PblObj {
1.60 - fmz = Formalise.empty, origin = (O_Model.empty, References.empty, TermC.empty),
1.61 - spec = (thy_id, probl_id, meth_id), probl = check_input model, meth = []: Model_Def.i_model,
1.62 - ctxt = ContextC.empty, loc = (NONE, NONE),
1.63 - branch = Ctree.NoBranch, ostate = Ctree.Incomplete, result = (TermC.empty, [])}, [])
1.64 - | update_state (model, (thy_id, probl_id, meth_id)) (*TODO +switch RProblem | RMethod*)
1.65 +(*at the first encounter of an Example
1.66 + transfer Example to ctree:
1.67 + origin: eventually used by sub-problems, too
1.68 + O_Model: for check of missing items
1.69 + I_Model: for efficient check of user input
1.70 +*)
1.71 +\<close> ML \<open>
1.72 +\<close> ML \<open>
1.73 +\<close> ML \<open>
1.74 +\<close> ML \<open>
1.75 +\<close> ML \<open>
1.76 +fun init_ctree example_id =
1.77 + let
1.78 + val (_, (fmz as (model, refs as (_(*thy_id*), probl_id, _)))) = get_example example_id
1.79 + val o_model = (* TODO works only within Isac_Test_Base ---vvvvvvvvvvvvvvv *)
1.80 + (*Problem.from_store probl_id |> #ppc |> O_Model.init model (ThyC.get_theory thy_id)*)
1.81 + Problem.from_store probl_id |> #ppc |> O_Model.init model @{theory Diff_App}
1.82 + in
1.83 + Ctree.Nd (Ctree.PblObj {
1.84 + fmz = fmz, origin = (o_model, refs, TermC.empty (*TODO handle CAS_Cmd*)),
1.85 + spec = References.empty, probl = I_Model.empty, meth = I_Model.empty,
1.86 + ctxt = ContextC.empty, loc = (NONE, NONE),
1.87 + branch = Ctree.NoBranch, ostate = Ctree.Incomplete, result = (TermC.empty, [])}, [])
1.88 + end
1.89 +\<close> ML \<open>
1.90 +\<close> ML \<open>
1.91 +fun update_state (example_id, _) Ctree.EmptyPtree = init_ctree example_id
1.92 + (*TODO +switch RProblem | RMethod*)
1.93 + | update_state (_, (model, (thy_id, probl_id, meth_id)))
1.94 (Ctree.Nd (Ctree.PblObj {fmz, origin, spec = _, probl = _, meth, ctxt, loc, branch, ostate, result},
1.95 children)) =
1.96 Ctree.Nd (Ctree.PblObj {
1.97 @@ -91,8 +128,7 @@
1.98 branch = branch, ostate = ostate, result = result}, children)
1.99 | update_state _ _ = raise ERROR "update_state: uncovered case in fun.def."
1.100 \<close> ML \<open>
1.101 -update_state: Problem.model_input * (ThyC.id * Problem.id * MethodC.id)
1.102 - -> Ctree.ctree -> Ctree.ctree
1.103 +update_state: example_id * (Problem.model_input * References.T) -> Ctree.ctree -> Ctree.ctree
1.104 \<close> ML \<open>
1.105 type references_input = (string * (string * string))
1.106 \<close> ML \<open>
1.107 @@ -116,12 +152,12 @@
1.108 Parse.!!! ( \<^keyword>\<open>Specification\<close> -- \<^keyword>\<open>:\<close> --
1.109 \<^keyword>\<open>Model\<close> -- \<^keyword>\<open>:\<close> |-- Problem.parse_model_input --
1.110 Parse.!!! ( \<^keyword>\<open>References\<close> -- \<^keyword>\<open>:\<close> |-- (*parse_references_input*)Problem.parse_cas))) >>
1.111 - (fn (_(*exp_id*), (_(*probl_id'*), (model_input, _(*references_input*)))) =>
1.112 + (fn (example_id, (_(*probl_id'*), (model_input, _(*references_input*)))) =>
1.113 Toplevel.theory (fn thy =>
1.114 let
1.115 val (thy_id, (probl_id, meth_id)) = (*references_input*)("Diff_App", ("univariate_calculus/Optimisation", "Optimisation/by_univariate_calculus"))
1.116 - val input = update_state (model_input,
1.117 - (thy_id, References_Def.explode_id probl_id, References_Def.explode_id meth_id))
1.118 + val input = update_state (example_id, (model_input,
1.119 + (thy_id, References_Def.explode_id probl_id, References_Def.explode_id meth_id)))
1.120 Ctree.EmptyPtree;
1.121 in set_data input thy end)));
1.122 \<close> ML \<open>