1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Tools/isac/BridgeJEdit/template.sml Wed Feb 22 18:40:34 2023 +0100
1.3 @@ -0,0 +1,119 @@
1.4 +(* Title: BridgePIDE/template.sml
1.5 + Author:
1.6 +
1.7 + 1. The keyword \<open>Example\<close> shall insert the template underneath
1.8 + 2. The template is filled from hidden data:
1.9 + 2.1. \<open>Model\<close>:
1.10 + The elements come with hints for input the format,
1.11 + see test/../i-model.sml --- build I_Model.init_TEST ---
1.12 + 2.2 \<open>References\<close>:
1.13 + * The elements come with hints for input the format, see test/../Test_VSCode_Example.thy
1.14 + * toggle \<Odot>\<Otimes> determines whether the \<open>Model\<close> relates to \<open>Problem_Ref\<close> or \<open>Method_Ref\<close>
1.15 + 3. Input to 2.1 is
1.16 + * checked and marked with feedback
1.17 + * datatype feedback = Correct | Incomplete | SyntaxError | Superfluous | False
1.18 + 4. Input to 2.2 eventually by selection from a tree (a DAG for theories)
1.19 +*)
1.20 +
1.21 +signature TEMPLATE =
1.22 +sig
1.23 + datatype model_for = Problem | Method
1.24 + datatype feedback = Correct | Incomplete | SyntaxError | Superfluous | False
1.25 +
1.26 + val show: Proof.context -> (bool * term) list -> I_Model.T_TEST -> References.input -> unit
1.27 +
1.28 +(*from isac_test for Minisubpbl*)
1.29 + type model_out
1.30 + val model_to_string: model_out -> string
1.31 + val refs_to_string: References.input -> string
1.32 + val model_to_out: Proof.context -> (bool * term) list -> I_Model.T_TEST -> model_out
1.33 +
1.34 +\<^isac_test>\<open>
1.35 +(**)
1.36 +\<close>
1.37 +end
1.38 +
1.39 +(**)
1.40 +structure Template(**) : TEMPLATE(**) =
1.41 +struct
1.42 +(**)
1.43 +
1.44 +datatype model_for = Problem | Method
1.45 +datatype feedback = Correct | Incomplete | SyntaxError | Superfluous | False
1.46 +type item_out = UnparseC.term_as_string * feedback
1.47 +type field_out = Model_Pattern.m_field * item_out list
1.48 +type model_out =
1.49 + field_out (* "#Given", feedback: Correct | Incomplete | SyntaxError | Superfluous *)
1.50 + * field_out (* "#Where", feedback: Correct | False *)
1.51 + * field_out (* "#Given", feedback: Correct | Incomplete | SyntaxError | Superfluous *)
1.52 + * field_out (* "#Given", feedback: Correct | Incomplete | SyntaxError | Superfluous *)
1.53 +
1.54 +
1.55 +(** create strings **)
1.56 +
1.57 +fun feedback_to_string Correct = " (Correct)"
1.58 + | feedback_to_string Incomplete = " (Incomplete)"
1.59 + | feedback_to_string SyntaxError = " (SyntaxError)"
1.60 + | feedback_to_string Superfluous = " (Superfluous)"
1.61 + | feedback_to_string False = " (False)"
1.62 +fun elem_to_string false (term_as_string, fb) =
1.63 + quote term_as_string ^ feedback_to_string fb ^ "\n"
1.64 + | elem_to_string true (term_as_string, fb) =
1.65 + " " ^ quote term_as_string ^ feedback_to_string fb ^ "\n"
1.66 +fun field_to_string (m_field, []) = m_field ^ ": \n"
1.67 + | field_to_string (m_field, elem :: elems) =
1.68 + m_field ^ ": " ^ elem_to_string false elem ^
1.69 + fold (curry op ^) (map (elem_to_string true) (elems)) ""
1.70 +fun model_to_string (given, where_, find, relate) =
1.71 + " Specification:\n" ^
1.72 + " Model:\n" ^
1.73 + " " ^ field_to_string given ^
1.74 + " " ^ field_to_string where_ ^
1.75 + " " ^ field_to_string find ^
1.76 + " " ^ field_to_string relate (*^
1.77 + " References:\n"*)
1.78 +
1.79 +
1.80 +(** create output format **)
1.81 +
1.82 +fun item_to_out ctxt (_, _, _, _, (_, I_Model.Cor_TEST (dsc_ts, _))) =
1.83 + (dsc_ts |> Term.list_comb |> UnparseC.term ctxt, Correct)
1.84 + | item_to_out ctxt (_, _, _, _, (_, I_Model.Inp_TEST (dsc, format))) =
1.85 + (UnparseC.term ctxt dsc ^ " " ^ format, Incomplete)
1.86 + | item_to_out _ (_, _, _, _, (_, I_Model.Syn_TEST (term_as_string))) =
1.87 + (term_as_string, Incomplete)
1.88 + | item_to_out ctxt (_, _, _, _, (_, I_Model.Inc_TEST (dsc_ts, _))) =
1.89 + (dsc_ts |> Term.list_comb |> UnparseC.term ctxt, Incomplete)
1.90 + | item_to_out ctxt (_, _, _, _, (_, I_Model.Sup_TEST dsc_ts)) =
1.91 + (dsc_ts |> Term.list_comb |> UnparseC.term ctxt, Superfluous)
1.92 +fun items_to_out ctxt m_field items =
1.93 + (m_field,
1.94 + filter (fn (_, _, _, f, _) => f = m_field) items |> map (item_to_out ctxt))
1.95 +fun where_to_out ctxt (bool, t) =
1.96 + (UnparseC.term ctxt t, if bool then Correct else False)
1.97 +fun wheres_to_out ctxt wheres = ("#Where", map (where_to_out ctxt) wheres)
1.98 +fun model_to_out ctxt where_ model =
1.99 + let
1.100 + val given = items_to_out ctxt "#Given" model
1.101 + val where_ = wheres_to_out ctxt where_
1.102 + val find = items_to_out ctxt "#Find" model
1.103 + val relate = items_to_out ctxt "#Relate" model
1.104 + in (given, where_, find, relate) end
1.105 +fun refs_to_string (thy, pbl, met) =
1.106 + " References:\n" ^
1.107 + " Theory_Ref: " ^ quote thy ^ "\n" ^
1.108 + " Problem_Ref: " ^ quote pbl ^ "\n" ^
1.109 + " Method_Ref: " ^ quote met ^ "\n" ^
1.110 + " Solution:"
1.111 +
1.112 +
1.113 +(** a fake version for Template.show **)
1.114 +
1.115 +fun show ctxt precond i_model in_refs =
1.116 + let
1.117 + val model_out = model_to_out ctxt precond i_model
1.118 + val fake_string = model_to_string model_out ^ refs_to_string in_refs
1.119 + val _ = writeln fake_string
1.120 + in () end
1.121 +
1.122 +(**)end(*struct*);
1.123 \ No newline at end of file
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/test/Tools/isac/BridgeJEdit/template.sml Wed Feb 22 18:40:34 2023 +0100
2.3 @@ -0,0 +1,90 @@
2.4 +(* Title: "BridgeJEdit/template.sml"
2.5 + Author: Walther Neuper
2.6 +*)
2.7 +
2.8 +"-----------------------------------------------------------------------------------------------";
2.9 +"table of contents -----------------------------------------------------------------------------";
2.10 +"-----------------------------------------------------------------------------------------------";
2.11 +"----------- build Template.show ---------------------------------------------------------------";
2.12 +"-----------------------------------------------------------------------------------------------";
2.13 +"-----------------------------------------------------------------------------------------------";
2.14 +"-----------------------------------------------------------------------------------------------";
2.15 +
2.16 +open Template;
2.17 +"----------- build Template.show ---------------------------------------------------------------";
2.18 +"----------- build Template.show ---------------------------------------------------------------";
2.19 +"----------- build Template.show ---------------------------------------------------------------";
2.20 +(*/---------------------------------------- mimic input from PIDE -----------------------------\*)
2.21 +
2.22 +(* Test_Example "Diff_App-No.123a" (*complete Model, empty References*) *)
2.23 +val in_refs as (thy_id, probl_id, meth_id) = ("__", "__/__", "__/__")
2.24 +val thy = @{theory}
2.25 +val model_input = (*type Position.T is hidden, thus redefinition*)
2.26 + [("#Given", [("Constants [r = 7]", Position.none)]),
2.27 + ("#Where", [("0 < r", Position.none)]),
2.28 + ("#Find",
2.29 + [("Maximum A", Position.none), ("AdditionalValues [u, v]", Position.none)]),
2.30 + ("#Relate",
2.31 + [("Extremum (A = 2 * u * v - u \<up> 2)", Position.none),
2.32 + ("SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]", Position.none)])]
2.33 +: (Model_Pattern.m_field * (string * Position.T) list) list
2.34 +val example_id = "Diff_App-No.123a";
2.35 +(*----------------------------------------- init state -----------------------------------------*)
2.36 +set_data Ctree.EmptyPtree @{theory Calculation};
2.37 +(*\---------------------------------------- mimic input from PIDE -----------------------------/*)
2.38 +
2.39 +val Ctree.EmptyPtree =
2.40 + (*case*) the_data @{theory Calculation} (*of*);
2.41 +
2.42 +(* Calculation.thy..*)
2.43 +"~~~~~ fun init_ctree_TEST , args:"; val (thy, example_id) = (thy, example_id);
2.44 + val user_ctxt = Proof_Context.init_global thy
2.45 + val example_id' = References_Def.explode_id example_id
2.46 + val (_, (formalise as (model, refs as (thy_id, probl_id, meth_id)))) =
2.47 + Store.get (Know_Store.get_expls @{theory}) example_id' example_id'
2.48 + val calc_thy = ThyC.get_theory user_ctxt thy_id
2.49 + val {model = model_patt, ...} = Problem.from_store user_ctxt probl_id
2.50 + val (o_model, ctxt) = O_Model.init calc_thy model model_patt
2.51 +;
2.52 +(*+*)o_model: O_Model.T; (* |> O_Model.to_string @{context}*)
2.53 +(*+*)val "Diff_App" = ctxt |> Proof_Context.theory_of |> ThyC.id_of
2.54 +(*+*)val ("Diff_App", ["univariate_calculus", "Optimisation"], ["Optimisation", "by_univariate_calculus"]) =
2.55 +(*+*) refs
2.56 +
2.57 + val empty_i_model = I_Model.init_TEST model_patt;
2.58 +
2.59 +(*+*)if I_Model.to_string_TEST @{context} empty_i_model =
2.60 +(*+*) "[\n(0, [], false ,#Given, (Position.T, Inp_TEST Constants [__=__, __=__])), \n" ^
2.61 +(*+*) "(0, [], false ,#Find, (Position.T, Inp_TEST Maximum __)), \n" ^
2.62 +(*+*) "(0, [], false ,#Find, (Position.T, Inp_TEST AdditionalValues [__, __])), \n" ^
2.63 +(*+*) "(0, [], false ,#Relate, (Position.T, Inp_TEST Extremum __)), \n" ^
2.64 +(*+*) "(0, [], false ,#Relate, (Position.T, Inp_TEST SideConditions [__=__, __=__]))]"
2.65 +(*+*)then () else error "final test of build I_Model.init_TEST FAILED";
2.66 +
2.67 + val {where_rls, where_, ...} = MethodC.from_store ctxt meth_id; (*..MethodC ?*)
2.68 + val (_, preconds) = Pre_Conds.check ctxt where_rls where_ [(*TODO: I_Model.T_TEST*)] 0;
2.69 +
2.70 + show ctxt preconds empty_i_model in_refs;
2.71 +"~~~~~ fun show , args:"; val (ctxt, preconds, i_model, in_refs) =
2.72 + (ctxt, preconds, empty_i_model, in_refs);
2.73 +(*let*)
2.74 + val model_out = model_to_out ctxt preconds i_model
2.75 + val fake_string = model_to_string model_out ^ refs_to_string in_refs
2.76 + val _ = writeln fake_string
2.77 +;
2.78 + ()
2.79 +;
2.80 +if fake_string =
2.81 + " Specification:\n" ^
2.82 + " Model:\n" ^
2.83 + " #Given: \"Constants [__=__, __=__]\" (Incomplete)\n" ^
2.84 + " #Where: \n" ^
2.85 + " #Find: \"Maximum __\" (Incomplete)\n" ^
2.86 + " \"AdditionalValues [__, __]\" (Incomplete)\n" ^
2.87 + " #Relate: \"Extremum __\" (Incomplete)\n" ^
2.88 + " \"SideConditions [__=__, __=__]\" (Incomplete)\n" ^
2.89 + " References:\n Theory_Ref: \"__\"\n" ^
2.90 + " Problem_Ref: \"__/__\"\n" ^
2.91 + " Method_Ref: \"__/__\"\n" ^
2.92 + " Solution:"
2.93 +then () else error "final test of build Template.show CHANGED"
3.1 --- a/test/Tools/isac/Test_Isac_Short.thy Wed Feb 22 18:38:56 2023 +0100
3.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Wed Feb 22 18:40:34 2023 +0100
3.3 @@ -304,7 +304,7 @@
3.4 (** ) (* evaluated in Build_Isac.thy already *)
3.5 ML_file "BridgeJEdit/e-collect.sml"
3.6 ML_file "BridgeJEdit/user-model.sml"
3.7 -(*ML_file "BridgeJEdit/template.sml"*)
3.8 + ML_file "BridgeJEdit/template.sml"
3.9 ML_file "BridgeJEdit/preliminary.sml"
3.10 ML_file "BridgeJEdit/vscode-example.sml"
3.11 ( **)