1 (* Title: src/Tools/isac/BridgeJEdit/Calculation.thy
2 Author: Walther Neuper, JKU Linz
4 Outer syntax for Isabelle/Isac's Calculation interactive via Isabelle/PIDE.
5 Second trial following Makarius' definition of "problem" already existing in this repository.
10 (**)"$ISABELLE_ISAC/Knowledge/Build_Thydata" (*remove after devel.of BridgeJEdit*)
11 (**)"$ISABELLE_ISAC/MathEngine/MathEngine"
12 (** )"SPARK_FDL" ( * remove after devel.of BridgeJEdit*)
13 keywords "Example" :: thy_decl
14 and "Problem" "Specification" "Model" "References" "Solution"
19 ML_file "preliminary.sml"
21 section \<open>new code for Outer_Syntax Example ...\<close>
23 stepwise development starts at changeset
24 https://hg.risc.uni-linz.ac.at/wneuper/isa/rev/9d98791b4080
25 and can be inspected following the subsequent changesets..
31 structure Data = Theory_Data
33 type T = Ctree.ctree option;
39 val set_data = Data.put o SOME;
41 case Data.get thy of NONE => Ctree.EmptyPtree
42 | SOME ctree => ctree;
45 A provisional Example collection.
47 For notes from ISAC's discontinued Java front-end see
48 https://isac.miraheze.org/wiki/Extend_ISAC_Knowledge#Add_an_example_in_XML_format
50 type description = string
51 type example = (description * Formalise.T)
52 type example_id = string
53 val example_store = Unsynchronized.ref ([]: (example_id * example) list)
54 fun get_example example_id =
55 case AList.lookup op= (!example_store) example_id of
56 NONE => raise ERROR ("Examnple " ^ quote example_id ^ " not found")
59 get_example: example_id -> example;
61 example_store := AList.update op= ("Diff_App/No.123 a",
62 ("The efficiency of an electrical coil depends on the mass of the kernel." ^
63 "Given is a kernel with cross-sectional area determined by two rectangles" ^
64 "of same shape as shown in the figure." ^
65 "Given a radius r = 7, determine the length u and width v of the rectangles" ^
66 "such that the cross-sectional area A (and thus the mass of the kernel) is a" ^
70 "Constants [r = (7::real)]", "Maximum A", "AdditionalValues [u, v]",
71 "Extremum (A = 2 * u * v - u \<up> 2)",
72 "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]",
73 "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]",
74 "SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]",
76 "FunctionVariable a", "FunctionVariable b", "FunctionVariable \<alpha>",
79 "Domain {0 <..< \<pi> / 2}",
80 "ErrorBound (\<epsilon> = (0::real))"]: TermC.as_string list,
81 ("Diff_App", ["univariate_calculus", "Optimisation"],
82 ["Optimisation", "by_univariate_calculus"]): References.T)): example) (!example_store)
84 case get_example "Diff_App/No.123 a" of
85 (_, ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" :: _,
86 ("Diff_App", ["univariate_calculus", "Optimisation"] ,["Optimisation", "by_univariate_calculus"])))
88 | _ => error "intermed. example_store CHANGED";
91 fun check_input (*ctxt o-model ??*) (_: Problem.model_input) = []: I_Model.T
93 (*at the first encounter of an Example
94 transfer Example to ctree:
95 origin: eventually used by sub-problems, too
96 O_Model: for check of missing items
97 I_Model: for efficient check of user input
104 fun init_ctree example_id =
106 val (_, (fmz as (model, refs as (_(*thy_id*), probl_id, _)))) = get_example example_id
107 val o_model = (* TODO works only within Isac_Test_Base ---vvvvvvvvvvvvvvv *)
108 (*Problem.from_store probl_id |> #ppc |> O_Model.init model (ThyC.get_theory thy_id)*)
109 Problem.from_store probl_id |> #ppc |> O_Model.init @{theory Diff_App} model
111 Ctree.Nd (Ctree.PblObj {
112 fmz = fmz, origin = (o_model, refs, TermC.empty (*TODO handle CAS_Cmd*)),
113 spec = References.empty, probl = I_Model.empty, meth = I_Model.empty,
114 ctxt = ContextC.empty, loc = (NONE, NONE),
115 branch = Ctree.NoBranch, ostate = Ctree.Incomplete, result = (TermC.empty, [])}, [])
119 fun update_state (example_id, _) Ctree.EmptyPtree = init_ctree example_id
120 (*TODO +switch RProblem | RMethod*)
121 | update_state (_, (model, (thy_id, probl_id, meth_id)))
122 (Ctree.Nd (Ctree.PblObj {fmz, origin, spec = _, probl = _, meth, ctxt, loc, branch, ostate, result},
124 Ctree.Nd (Ctree.PblObj {
125 fmz = fmz, origin = origin,
126 spec = (thy_id, probl_id, meth_id), probl = check_input model, meth = meth,
127 ctxt = ctxt, loc = loc,
128 branch = branch, ostate = ostate, result = result}, children)
129 | update_state _ _ = raise ERROR "update_state: uncovered case in fun.def."
131 update_state: example_id * (Problem.model_input * References.T) -> Ctree.ctree -> Ctree.ctree
133 type references_input = (string * (string * string))
135 val parse_references_input =
136 Parse.!!! ( \<^keyword>\<open>Theory_Ref\<close> -- \<^keyword>\<open>Theory_Ref\<close> |-- Parse.name --
137 Parse.!!! ( \<^keyword>\<open>Problem_Ref\<close> -- \<^keyword>\<open>Theory_Ref\<close> |-- Parse.name --
138 Parse.!!! ( \<^keyword>\<open>Method_Ref\<close> -- \<^keyword>\<open>Theory_Ref\<close> |-- Parse.name)))
140 parse_references_input: references_input parser (*TODO: dpes not yet work,
141 thus in Outer_Syntax.command \<^command_keyword>\<open>Example\<close> replacced by Problem.parse_cas*)
143 op -- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e;
144 op |-- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'd * 'e
149 Outer_Syntax.command \<^command_keyword>\<open>Example\<close>
150 "prepare ISAC problem type and register it to Knowledge Store"
151 (Parse.name -- Parse.!!! ( \<^keyword>\<open>Problem\<close> |-- Parse.name --
152 Parse.!!! ( \<^keyword>\<open>Specification\<close> -- \<^keyword>\<open>:\<close> --
153 \<^keyword>\<open>Model\<close> -- \<^keyword>\<open>:\<close> |-- Problem.parse_model_input --
154 Parse.!!! ( \<^keyword>\<open>References\<close> -- \<^keyword>\<open>:\<close> |-- (*parse_references_input*)Problem.parse_cas))) >>
155 (fn (example_id, (_(*probl_id'*), (model_input, _(*references_input*)))) =>
156 Toplevel.theory (fn thy =>
158 val (thy_id, (probl_id, meth_id)) = (*references_input*)("Diff_App", ("univariate_calculus/Optimisation", "Optimisation/by_univariate_calculus"))
159 val input = update_state (example_id, (model_input,
160 (thy_id, References_Def.explode_id probl_id, References_Def.explode_id meth_id)))
162 in set_data input thy end)));
165 (*/----------------------------------------------------------------------------\*)
166 Parse.name -- Parse.!!! ( \<^keyword>\<open>Problem\<close> |-- Parse.name --
167 Parse.!!! ( \<^keyword>\<open>Specification\<close> -- \<^keyword>\<open>:\<close> --
168 \<^keyword>\<open>Model\<close> -- \<^keyword>\<open>:\<close> |-- Problem.parse_model_input --
169 Parse.!!! ( \<^keyword>\<open>References\<close> -- \<^keyword>\<open>:\<close> |-- parse_references_input)))
170 : (string * (string * (Problem.model_input * references_input))) parser
171 (*\----------------------------------------------------------------------------/*)
173 (*/----------------------------------------------------------------------------\*)
174 (string * (string * (Problem.model_input * references_input)))
175 (*\----------------------------------------------------------------------------/*)
177 (*/----------------------------------------------------------------------------\* )
178 the type above is the type of the argument of \<open>(fn (_(*name*),..\<close>
179 ( *\----------------------------------------------------------------------------/*)