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";
92 Implementation reasonable, as soo as
93 * clarified, how "empty" items in Model are represented
94 * parse_references_input works
95 * switching \<Odot>\<Otimes> i_model for probl and meth works.
97 fun check_input (*ctxt o-model ??*) (_: Problem.model_input) = []: I_Model.T (*TODO*)
100 (* at the first encounter of an Example create the following data and transfer them to ctree:
101 origin: eventually used by sub-problems, too
102 O_Model: for check of missing items
103 I_Model: for efficient check of user input
106 fun init_ctree example_id =
108 (* TODO vvvvvvvvvvvvvvv works only within Isac_Test_Base *)
109 val thy = (*ThyC.get_theory thy_id*)@{theory Diff_App}
110 val (_, (fmz as (model, refs as (_(*thy_id*), probl_id, _)))) = get_example example_id
111 val ctxt = ContextC.initialise' thy model;
113 val o_model = Problem.from_store probl_id |> #ppc |> O_Model.init thy model
115 Ctree.Nd (Ctree.PblObj {
116 fmz = fmz, origin = (o_model, refs, TermC.empty (*TODO handle CAS_Cmd*)),
117 spec = References.empty, probl = I_Model.empty, meth = I_Model.empty,
118 ctxt = ctxt, loc = (NONE, NONE),
119 branch = Ctree.NoBranch, ostate = Ctree.Incomplete, result = (TermC.empty, [])}, [])
124 * initialise ctree with origin from example_id
125 * add items already input ..TODO..TODO..TODO..TODO..TODO..TODO..TODO..TODO..TODO
128 fun update_state (example_id, (model, refs)) Ctree.EmptyPtree =
129 init_ctree example_id |> update_state (example_id, (model, refs))
130 | update_state (_, (model, (thy_id, probl_id, meth_id)))
131 (Ctree.Nd (Ctree.PblObj {fmz, origin, spec as (othy, opbl, omet), probl = _, meth, ctxt, loc, branch, ostate, result},
134 val _ = if thy_id <> othy then "re-parse all i_model" else "do nothing"
135 val _ = if probl_id <> opbl then "switch from meth? check_input of probl" else "do nothing"
136 val _ = if meth_id <> omet then "switch from probl check_input of meth" else "do nothing"
138 Ctree.Nd (Ctree.PblObj {
139 fmz = fmz, origin = origin, spec = References.select_input spec (thy_id, probl_id, meth_id),
140 probl = check_input model, meth = meth, (*TODO +switch Problem_Ref | Method_Ref*)
141 ctxt = ctxt, loc = loc,
142 branch = branch, ostate = ostate, result = result}, children)
144 | update_state _ _ = raise ERROR "update_state: uncovered case in fun.def"
148 update_state: example_id * (Problem.model_input * References.T) -> Ctree.ctree -> Ctree.ctree
150 type references_input = (string * (string * string))
152 val parse_references_input =
153 Parse.!!! ( \<^keyword>\<open>Theory_Ref\<close> -- \<^keyword>\<open>Theory_Ref\<close> |-- Parse.name --
154 Parse.!!! ( \<^keyword>\<open>Problem_Ref\<close> -- \<^keyword>\<open>Theory_Ref\<close> |-- Parse.name --
155 Parse.!!! ( \<^keyword>\<open>Method_Ref\<close> -- \<^keyword>\<open>Theory_Ref\<close> |-- Parse.name)))
157 parse_references_input: references_input parser (*TODO: dpes not yet work,
158 thus in Outer_Syntax.command \<^command_keyword>\<open>Example\<close> replacced by Problem.parse_cas*)
160 op -- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e;
161 op |-- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'd * 'e
167 val strl = Symbol.explode str |> rev
169 take (2, strl) = ["_", " "] orelse take (3, strl) = ["]", "_", "["]
172 val m2 = "0 < r"; val m2' = Symbol.explode m2 |> rev;
173 val m3 = "Maximum _"; val m3' = Symbol.explode m3 |> rev;
174 val m4 = "AdditionalValues [_]"; val m4' = Symbol.explode m4 |> rev;
178 Outer_Syntax.command \<^command_keyword>\<open>Example\<close>
179 "prepare ISAC problem type and register it to Knowledge Store"
180 (Parse.name -- Parse.!!! ( \<^keyword>\<open>Specification\<close> -- \<^keyword>\<open>:\<close> --
181 \<^keyword>\<open>Model\<close> -- \<^keyword>\<open>:\<close> |-- Problem.parse_model_input --
182 Parse.!!! ( \<^keyword>\<open>References\<close> -- \<^keyword>\<open>:\<close> |-- (*parse_references_input*) Problem.parse_cas)) >>
183 (fn (example_id, (model_input, _(*references_input*))) =>
184 Toplevel.theory (fn thy =>
187 val _ = writeln ("#Example model_input: " ^ @{make_string} model_input)
188 (* #Example model_input:
189 [("#Given", ["<markup>"]), ("#Where", ["<markup>"]), ("#Find", ["<markup>", "<markup>"]), ("#Relate", ["<markup>", "<markup>"])]*)
190 val [("#Given", [m1]), ("#Where", [m2]), ("#Find", [m3, m4]), ("#Relate", [m5, m6])] =
191 model_input : Problem.model_input
192 val _ = writeln ("#Example m.: " ^ m1 ^ " " ^ m2 ^ " " ^ m3 ^ " " ^ m4 ^ " " ^ m4 ^ " " ^ m5 ^ " " ^ m6)
194 val m2' = Symbol.explode m2;
195 val _ = writeln ("#Example Symbol.explode m2: " ^ @{make_string} m2')
196 val _ = if (is_empty m2) then writeln "true" else writeln "false";
197 val _ = if (is_empty m3) then writeln "true" else writeln "false";
198 val _ = if (is_empty m4) then writeln "true" else writeln "false";
199 (* #Example m.: Constants [r = 7] 0 < r Maximum _ AdditionalValues [_] AdditionalValues [_] Extremum _ SideCondition [_]*)
201 val (thy_id, (probl_id, meth_id)) = (*references_input*)("Diff_App", ("univariate_calculus/Optimisation", "Optimisation/by_univariate_calculus"))
202 val input = update_state (example_id, (model_input,
203 (thy_id, References_Def.explode_id probl_id, References_Def.explode_id meth_id)))
205 in set_data input thy end)));
208 (*/----------------------------------------------------------------------------\*)
209 Parse.name -- Parse.!!! ( \<^keyword>\<open>Problem\<close> |-- Parse.name --
210 Parse.!!! ( \<^keyword>\<open>Specification\<close> -- \<^keyword>\<open>:\<close> --
211 \<^keyword>\<open>Model\<close> -- \<^keyword>\<open>:\<close> |-- Problem.parse_model_input --
212 Parse.!!! ( \<^keyword>\<open>References\<close> -- \<^keyword>\<open>:\<close> |-- parse_references_input)))
213 : (string * (string * (Problem.model_input * references_input))) parser
214 (*\----------------------------------------------------------------------------/*)
216 (*/----------------------------------------------------------------------------\*)
217 (string * (string * (Problem.model_input * references_input)))
218 (*\----------------------------------------------------------------------------/*)
220 (*/----------------------------------------------------------------------------\* )
221 the type above is the type of the argument of \<open>(fn (_(*name*),..\<close>
222 ( *\----------------------------------------------------------------------------/*)
225 \<close> text \<open>
226 INVESTIGATE Problem.Outer_Syntax.command \ <^command_keyword>\<open>problem\<close>
227 on Biegelinie.problem pbl_bieg : "Biegelinien"
229 ML-source shows error-positions already perfectly: what types are involved?..
231 Rule_Set.append_rules "empty" Rule_Set.empty [] (* ORIGINAL source = ARGUMENT IN fn *)
233 Ouptut from Biegelinie.problem pbl_bieg : "Biegelinien":
234 #problem source: Source {delimited = true, range = ({offset=38, end_offset=87, id=-1652}, {offset=87, id=-1652}),
235 text = "\127Rule_Set.append_rules \"empty\" Rule_Set.empty []\127"}
238 val source = Input.empty;
239 val ml = ML_Lex.read;
241 (ml "Theory.setup (Problem.set_data (" @ ML_Lex.read_source source @ ml "))")
243 [Text (Token (({}, {}), (Long_Ident, "Theory.setup"))), Text (Token (({}, {}), (Space, " "))), Text (Token (({}, {}), (Keyword, "("))), Text (Token (({}, {}), (Long_Ident, "Problem.set_data"))),
244 Text (Token (({}, {}), (Space, " "))), Text (Token (({}, {}), (Keyword, "("))), Text (Token (({}, {}), (Space, " "))), Text (Token (({}, {}), (Keyword, ")"))), Text (Token (({}, {}), (Keyword, ")"))),
245 Text (Token (({}, {}), (Space, " ")))]
246 : ML_Lex.token Antiquote.antiquote list
247 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ type of (1a)
250 ML_Context.expression (Input.pos_of source)
251 (ml "Theory.setup (Problem.set_data (" @ ML_Lex.read_source source @ ml "))")
252 : Context.generic -> Context.generic
254 ML_Context.expression (Input.pos_of source)
255 (ml "Theory.setup (Problem.set_data (" @ ML_Lex.read_source source @ ml "))")
256 |> Context.theory_map
259 Outer_Syntax.command: Outer_Syntax.command_keyword -> string ->
260 (Toplevel.transition -> Toplevel.transition) parser -> unit
262 \<close> text \<open>
263 ML-source shows error-positions already perfectly: types involved are above.
265 Input at Given does NOT show error-position,
266 but ISAC msg \<open>ME_Isa: thy "Isac_Knowledge" not in system\<close>
268 Thus compare ML-source/input with model_input ...
270 Problem.parse_model_input: Problem.model_input parser;
271 Problem.parse_model_input: Token.src -> Problem.model_input * Token.src;
272 Problem.parse_model_input: Token.T list -> Problem.model_input * (Token.T list)
274 []: Position.range list;
278 (* Given: "Traegerlaenge l_l" "Streckenlast q_q" *)
280 Ouptut from Biegelinie.problem pbl_bieg : "Biegelinien":
281 #problem model_input: [("#Given", ["<markup>", "<markup>"]), ("#Find", ["<markup>"]), ("#Relate", ["<markup>"])]
282 : Problem.model_input
283 type of (1b) --------^^^^^^^^^^^^^^^^^^^^^^> contains ? Markup.T ?..
285 #problem m1: Traegerlaenge l_l
286 #problem m2: Streckenlast q_q
287 I this -----^^^______________^^^ Markup.T ?
289 \<close> ML \<open> (** investigate parse_model_input **)
290 \<close> ML \<open> (* how get a Token.T list without Outer_Syntax.command ? *)
292 Parse.term: string parser;
293 Parse.term: Token.T list -> string * Token.T list;
295 \<close> ML \<open> (* relation Token.T -- Markup.T ??? *)
297 val ctxt = Proof_Context.init_global @{theory};
298 val given_1 = Syntax.read_term ctxt "Traegerlaenge l_l" (* as in parse_tagged_terms *)
299 (* ^^^^^^^ : term -- why then evaluates parse_model_input to markup ? *)
302 Markup.literal_fact "Traegerlaenge l_l" = ("literal_fact", [("name", "Traegerlaenge l_l")])