1 (* Title: "BridgeJEdit/template.sml"
5 "-----------------------------------------------------------------------------------------------";
6 "table of contents -----------------------------------------------------------------------------";
7 "-----------------------------------------------------------------------------------------------";
8 "----------- build Template.show ---------------------------------------------------------------";
9 "-----------------------------------------------------------------------------------------------";
10 "-----------------------------------------------------------------------------------------------";
11 "-----------------------------------------------------------------------------------------------";
14 "----------- build Template.show ---------------------------------------------------------------";
15 "----------- build Template.show ---------------------------------------------------------------";
16 "----------- build Template.show ---------------------------------------------------------------";
17 (*/---------------------------------------- mimic input from PIDE -----------------------------\*)
19 (* Test_Example "Diff_App-No.123a" (*complete Model, empty References*) *)
20 val in_refs as (thy_id, probl_id, meth_id) = ("__", "__/__", "__/__")
22 val model_input = (*type Position.T is hidden, thus redefinition*)
23 [("#Given", [("Constants [r = 7]", Position.none)]),
24 ("#Where", [("0 < r", Position.none)]),
26 [("Maximum A", Position.none), ("AdditionalValues [u, v]", Position.none)]),
28 [("Extremum (A = 2 * u * v - u \<up> 2)", Position.none),
29 ("SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]", Position.none)])]
30 : (Model_Pattern.m_field * (string * Position.T) list) list
31 val example_id = "Diff_App-No.123a";
32 (*----------------------------------------- init state -----------------------------------------*)
33 set_data CTbasic_TEST.EmptyPtree @{theory Calculation};
34 (*\---------------------------------------- mimic input from PIDE -----------------------------/*)
36 val CTbasic_TEST.EmptyPtree =
37 (*case*) the_data @{theory Calculation} (*of*);
39 (* Calculation.thy..*)
40 "~~~~~ fun init_ctree , args:"; val (thy, example_id) = (thy, example_id);
41 val user_ctxt = Proof_Context.init_global thy
42 val example_id' = References_Def.explode_id example_id
43 val (_, (formalise as (model, refs as (thy_id, probl_id, meth_id)))) =
44 Store.get (Know_Store.get_expls @{theory}) example_id' example_id'
45 val calc_thy = ThyC.get_theory user_ctxt thy_id
46 val {model = model_patt, ...} = Problem.from_store user_ctxt probl_id
47 val (o_model, ctxt) = O_Model.init calc_thy model model_patt
49 (*+*)o_model: O_Model.T; (* |> O_Model.to_string @{context}*)
50 (*+*)val "Diff_App" = ctxt |> Proof_Context.theory_of |> ThyC.id_of
51 (*+*)val ("Diff_App", ["univariate_calculus", "Optimisation"], ["Optimisation", "by_univariate_calculus"]) =
54 val empty_i_model = I_Model.init_TEST o_model model_patt;
56 (*+*)if I_Model.to_string_TEST @{context} empty_i_model = "[\n" ^
57 (*+*) "(1, [1, 2, 3], false ,#Given, (Inc_TEST Constants [] [__=__, __=__], Position.T)), \n" ^
58 (*+*) "(2, [1, 2, 3], false ,#Find, (Inc_TEST Maximum __, Position.T)), \n" ^
59 (*+*) "(3, [1, 2, 3], false ,#Find, (Inc_TEST AdditionalValues [] [__, __], Position.T)), \n" ^
60 (*+*) "(4, [1, 2, 3], false ,#Relate, (Inc_TEST Extremum (__=__), Position.T)), \n" ^
61 (*+*) "(5, [1, 2], false ,#Relate, (Inc_TEST SideConditions [] [__=__, __=__], Position.T))]"
62 (*+*)then () else error "final test of build I_Model.init_TEST FAILED";
64 val {where_rls, where_, ...} = MethodC.from_store ctxt meth_id;
65 val (_, preconds) = Pre_Conds.check ctxt where_rls where_ (model_patt, empty_i_model);
67 show ctxt preconds empty_i_model in_refs;
68 "~~~~~ fun show , args:"; val (ctxt, preconds, i_model, in_refs) =
69 (ctxt, preconds, empty_i_model, in_refs);
70 (*+*)val "[\n(1, [1, 2, 3], false ,#Given, (Inc_TEST Constants [] [__=__, __=__], Position.T)), \n(2, [1, 2, 3], false ,#Find, (Inc_TEST Maximum __, Position.T)), \n(3, [1, 2, 3], false ,#Find, (Inc_TEST AdditionalValues [] [__, __], Position.T)), \n(4, [1, 2, 3], false ,#Relate, (Inc_TEST Extremum (__=__), Position.T)), \n(5, [1, 2], false ,#Relate, (Inc_TEST SideConditions [] [__=__, __=__], Position.T))]"
71 = i_model |> I_Model.to_string_TEST @{context}
74 model_to_out ctxt preconds i_model;
75 "~~~~~ fun model_to_out , args:"; val (ctxt, where_, model) = (ctxt, preconds, i_model);
78 items_to_out ctxt "#Given" model;
79 "~~~~~ fun items_to_out , args:"; val (ctxt, m_field, items) = (ctxt, "#Given", model);
81 val return_ = (m_field, filter (fn (_, _, _, f, _) => f = m_field) items |>
82 map (item_to_out ctxt));
83 "~~~~~ fun item_to_out , args:"; val (ctxt, (_, _, _, _, (I_Model.Inc_TEST ((dsc, [])), _))) =
85 val return_ = (UnparseC.term ctxt dsc ^ " " ^ Model_Pattern.empty_for dsc, Incomplete)
87 (*+*)val ("Constants [__=__, __=__]", Incomplete) = return_
88 (*|------------------- contine show ----------------------------------------------------------*)
89 val fake_string = model_to_string model_out ^ refs_to_string in_refs
90 val _ = writeln fake_string
95 " #Given: \"Constants [__=__, __=__]\" (Incomplete)\n" ^
97 " #Find: \"Maximum __\" (Incomplete)\n" ^
98 " \"AdditionalValues [__, __]\" (Incomplete)\n" ^
99 " #Relate: \"Extremum (__=__)\" (Incomplete)\n" ^
100 " \"SideConditions [__=__, __=__]\" (Incomplete)\n" ^
101 " References:\n Theory_Ref: \"__\"\n" ^
102 " Problem_Ref: \"__/__\"\n" ^
103 " Method_Ref: \"__/__\"\n" ^
105 then () else error "final test of build Template.show CHANGED"