1.1 --- a/TODO.md Fri Dec 09 16:29:04 2022 +0100
1.2 +++ b/TODO.md Thu Dec 15 13:03:51 2022 +0100
1.3 @@ -2,8 +2,6 @@
1.4 with separator \<^medskip> and some tool support for automated
1.5 update (in "isabelle update" and/or PIDE);
1.6
1.7 -* MW?: rename *.sml to *.ML, potentially with tool support;
1.8 -
1.9 * MW: implement a template for der Specification
1.10
1.11 * MW: clarify/eliminate Isabelle/Scala add-ons (presently unused)
1.12 @@ -44,7 +42,6 @@
1.13
1.14 ***** priority of WN items is top down, most urgent/simple on top
1.15
1.16 -* WN?: improve Problem/MethodC..prep_input after meeting MW
1.17 * WN: eliminate multiple get_ctxt in Solve_Step, Ctree
1.18 * WN: shift code from libraryC.sml to designated destination (ThyC, etc)
1.19 * WN: Know_Store.get_thes, add_thes still required for Error_Patterns, we want to eliminate thes:
2.1 --- a/src/Tools/isac/BaseDefinitions/model-pattern.sml Fri Dec 09 16:29:04 2022 +0100
2.2 +++ b/src/Tools/isac/BaseDefinitions/model-pattern.sml Thu Dec 15 13:03:51 2022 +0100
2.3 @@ -12,15 +12,15 @@
2.4 type T
2.5 type single
2.6 val to_string: single list -> string
2.7 +
2.8 + type model_input_pos
2.9 type pre_model
2.10 - type model_input_pos
2.11 + type pre_model_single
2.12
2.13 type m_field = string
2.14 type descriptor = term
2.15 - val split_descriptor: Proof.context -> m_field * term -> m_field * (descriptor * term)
2.16 - val split_model: Proof.context -> pre_model -> T
2.17 -
2.18 - val parse: Proof.context -> model_input_pos -> pre_model * term list
2.19 + val parse_pos: Proof.context -> (m_field * (string * Position.T) list) list ->
2.20 + pre_model * (term * Position.T) list
2.21
2.22 val variables: T -> term list
2.23 val get_field: descriptor -> T -> m_field option
2.24 @@ -31,6 +31,11 @@
2.25 val adapt_to_type_int: term -> term
2.26
2.27 \<^isac_test>\<open>
2.28 + val split_descriptor: Proof.context -> m_field * term * Position.T -> pre_model_single
2.29 + val parse_term: Proof.context -> m_field * ((*TermC.as_*)string * Position.T) ->
2.30 + m_field * term * Position.T
2.31 + val parse_pattern: Proof.context -> m_field * ((*TermC.as_*)string * Position.T) ->
2.32 + m_field * term * Position.T
2.33 val to_string': T -> string
2.34 \<close>
2.35 end
2.36 @@ -50,38 +55,43 @@
2.37 (* does NOT contain pre-conditions, because these have no \<open>descriptor\<close> *)
2.38 type T = single list;
2.39
2.40 -type pre_model = (m_field * term) list
2.41 type model_input_pos = (string * (string * Position.T) list) list
2.42 +type pre_model_single = (m_field * (descriptor * term) * Position.T)
2.43 +type pre_model = (m_field * (term * term) * Position.T) list
2.44
2.45 -fun split_descriptor ctxt (m_field, dsc_tm) =
2.46 +(*val split_descriptor: Proof.context -> m_field * term * Position.T ->
2.47 + m_field * (descriptor * term)(* * Position.T*)*)
2.48 +fun split_descriptor ctxt (m_field: string, dsc_tm, pos) =
2.49 let
2.50 - val (hd, arg) = case strip_comb dsc_tm of
2.51 + val (m_field, (hd, arg)) = case strip_comb dsc_tm of
2.52 (hd, [arg]) => (m_field, (hd, arg))
2.53 - | _ => raise ERROR ("Model_Pattern.split_descriptor: doesn't match (hd,[arg]) for t = " ^
2.54 - quote (UnparseC.term_in_ctxt ctxt dsc_tm))
2.55 - in (hd, arg) end
2.56 + | _ => error ("Wrong descriptor " ^ quote (UnparseC.term_in_ctxt ctxt dsc_tm) ^ Position.here pos)
2.57 + in (m_field, (hd, arg), pos) end
2.58
2.59 -fun split_model ctxt (gi_fi_re) = map (split_descriptor ctxt) gi_fi_re
2.60
2.61 (*val parse_term: Proof.context -> m_field * ((*TermC.as_*)string * Position.T) -> m_field * term*)
2.62 fun parse_term ctxt (m_field, (str, pos)) =
2.63 (m_field,
2.64 (Syntax.read_term ctxt str
2.65 - handle ERROR msg => error (msg ^ Position.here pos)))
2.66 + handle ERROR msg => error (msg ^ Position.here pos)),
2.67 + pos)
2.68 fun parse_pattern ctxt (m_field, (str, pos)) =
2.69 (m_field,
2.70 (Proof_Context.read_term_pattern ctxt str
2.71 - handle ERROR msg => error (msg ^ Position.here pos)))
2.72 -fun parse ctxt model_input =
2.73 + handle ERROR msg => error (msg ^ Position.here pos)),
2.74 + pos)
2.75 +
2.76 +fun parse_pos ctxt model_input =
2.77 let
2.78 val items = model_input |> map (fn (m_field, items) => map (pair m_field) items) |> flat;
2.79 val model = items
2.80 |> filter_out ((fn f => (fn (f', _) => f = f')) "#Where")
2.81 |> map (parse_term ctxt)
2.82 + |> map (split_descriptor ctxt)
2.83 val where_ = items
2.84 |> filter ((fn f => (fn (f', _) => f = f')) "#Where")
2.85 |> map (parse_pattern ctxt)
2.86 - |> map snd
2.87 + |> map (fn (_, a, b) => (a, b))
2.88 in (model, where_) end
2.89
2.90 fun pat2str (field, (dsc, id)) = pair2str (field, pair2str (UnparseC.term dsc, UnparseC.term id));
3.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy Fri Dec 09 16:29:04 2022 +0100
3.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy Thu Dec 15 13:03:51 2022 +0100
3.3 @@ -114,9 +114,9 @@
3.4 "~~~~~ fun collect_part , args:"; val (part, parent, thys) = ("IsacKnowledge", knowledge_parent, knowthys');
3.5 \<close> ML \<open>
3.6 val xxx = (flat (map (Thy_Hierarchy.collect_thms part) thys))
3.7 -\<close> ML \<open> (*isa*)
3.8 -length thys = 32;
3.9 -length xxx = 471
3.10 +\<close> ML \<open>
3.11 +val 34 = length thys;
3.12 +val 479 = length xxx;
3.13 \<close> text \<open>
3.14 (collect_rlss part (Know_Store.get_rlss parent) thys)
3.15 \<close> text \<open>
4.1 --- a/src/Tools/isac/Knowledge/LinEq.thy Fri Dec 09 16:29:04 2022 +0100
4.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Thu Dec 15 13:03:51 2022 +0100
4.3 @@ -150,7 +150,7 @@
4.4 errpats = [], rew_rls = norm_Poly}\<close>
4.5 Program: solve_linear_equation.simps
4.6 Given: "equality e_e" "solveFor v_v"
4.7 - Where: "Not ((lhs e_e) is_polyrat_in v_v)" "((lhs e_e) has_degree_in v_v) = 1"
4.8 + Where: "Not ((lhs e_e) is_polyrat_in v_v)" "((lhs e_e) has_degree_in v_v) = 1"
4.9 Find: "solutions v_v'i'"
4.10
4.11 section \<open>For trials\<close>
5.1 --- a/src/Tools/isac/MathEngBasic/method.sml Fri Dec 09 16:29:04 2022 +0100
5.2 +++ b/src/Tools/isac/MathEngBasic/method.sml Thu Dec 15 13:03:51 2022 +0100
5.3 @@ -20,7 +20,8 @@
5.4
5.5 type ml_input
5.6 val prep_store: theory -> Check_Unique.id -> string list -> References_Def.id ->
5.7 - id * Model_Pattern.pre_model * term list * ml_input * thm -> T * id(**)
5.8 + id * (Model_Pattern.m_field * (Model_Pattern.descriptor * term)) list * term list * ml_input * thm ->
5.9 + T * id
5.10
5.11 val set_data: ml_input -> theory -> theory
5.12 val the_data: theory -> ml_input
5.13 @@ -53,13 +54,10 @@
5.14 {rew_ord = ro, rls' = rls, prog_rls = prog_rls, where_rls = where_rls, calc = _(*scr_isa_fns*),
5.15 errpats = ep, rew_rls = nr}, prog) =
5.16 let
5.17 - val ctxt = Proof_Context.init_global thy
5.18 -
5.19 - val model' = Model_Pattern.split_model ctxt model
5.20 val sc = Program.prep_program prog
5.21 val calc = if Thm.eq_thm (prog, @{thm refl}) then [] else Auto_Prog.get_calcs thy sc
5.22 in
5.23 - ({guh = guh, mathauthors = mathauthors, start_refine = start_refine, model = model',
5.24 + ({guh = guh, mathauthors = mathauthors, start_refine = start_refine, model = model(*'*),
5.25 where_ = where_, rew_ord = ro, asm_rls = rls, prog_rls = prog_rls, where_rls = where_rls,
5.26 calc = calc, errpats = ep, rew_rls = nr, program = Rule.Prog sc}: T, met_id)
5.27 end;
5.28 @@ -78,6 +76,9 @@
5.29
5.30 local
5.31
5.32 +val drop_pos_model = (fn (a, b, _) => (a, b))
5.33 +val drop_pos_where_ = (fn (b, _) => b)
5.34 +
5.35 val parse_program =
5.36 Scan.option (Problem.parse_item \<^keyword>\<open>Program\<close> (Parse.position Parse.name));
5.37
5.38 @@ -93,7 +94,8 @@
5.39 let
5.40 val ctxt = Proof_Context.init_global thy
5.41 val met_id = References_Def.explode_id id;
5.42 - val (model, where_) = Model_Pattern.parse ctxt model_input
5.43 + val (model, where_) = Model_Pattern.parse_pos ctxt model_input
5.44 + val (model', where_') = (map drop_pos_model model, map drop_pos_where_ where_)
5.45 val set_data =
5.46 ML_Context.expression (Input.pos_of source)
5.47 (ml "Theory.setup (MethodC.set_data (" @ ML_Lex.read_source source @ ml "))")
5.48 @@ -103,7 +105,7 @@
5.49 (case program of
5.50 NONE => @{thm refl}
5.51 | SOME a => Global_Theory.get_thm thy (Global_Theory.check_fact thy a));
5.52 - val arg = prep_store thy name maa id_empty (met_id, model, where_, ml_input, thm);
5.53 + val arg = prep_store thy name maa id_empty (met_id, model', where_', ml_input, thm);
5.54 in Know_Store.add_mets ctxt [arg] thy end)))
5.55
5.56 in end;
6.1 --- a/src/Tools/isac/MathEngBasic/problem.sml Fri Dec 09 16:29:04 2022 +0100
6.2 +++ b/src/Tools/isac/MathEngBasic/problem.sml Thu Dec 15 13:03:51 2022 +0100
6.3 @@ -21,8 +21,9 @@
6.4
6.5 type model_input_pos
6.6 val prep_store: theory -> Check_Unique.id -> string list -> References_Def.id ->
6.7 - Model_Pattern.pre_model * term list * term option -> id * References_Def.id list * Rule_Set.T ->
6.8 - T * id
6.9 + (Model_Pattern.m_field * (Model_Pattern.descriptor * term)) list * term list * term option ->
6.10 + id * References_Def.id list * Rule_Set.T -> T * id
6.11 +
6.12 val set_data: Rule_Def.rule_set -> theory -> theory
6.13 val the_data: theory -> Rule_Def.rule_set
6.14
6.15 @@ -67,12 +68,8 @@
6.16 list; (* list of "#Given" .. "#Relate" *)
6.17
6.18 fun prep_store thy name maa start_refine (model, where_, cas) (pbl_id, met_ids, where_rls) =
6.19 - let
6.20 - val model' = Model_Pattern.split_model (Proof_Context.init_global thy) model
6.21 - in
6.22 - ({guh = name, mathauthors = maa, start_refine = start_refine, thy = thy, cas = cas,
6.23 - where_rls = where_rls, where_ = where_, model = model', solve_mets = met_ids}, pbl_id)
6.24 - end
6.25 + ({guh = name, mathauthors = maa, start_refine = start_refine, thy = thy, cas = cas,
6.26 + where_rls = where_rls, where_ = where_, model = model, solve_mets = met_ids}, pbl_id)
6.27
6.28
6.29 (** Isar command **)
6.30 @@ -125,6 +122,9 @@
6.31
6.32 local
6.33
6.34 +val drop_pos_model = (fn (a, b, _) => (a, b))
6.35 +val drop_pos_where_ = (fn (b, _) => b)
6.36 +
6.37 val _ =
6.38 Outer_Syntax.command \<^command_keyword>\<open>problem\<close>
6.39 "prepare ISAC problem type and register it to Knowledge Store"
6.40 @@ -137,15 +137,16 @@
6.41 val ctxt = Proof_Context.init_global thy
6.42 val pbl_id = References_Def.explode_id id;
6.43 val met_ids = map References_Def.explode_id mets;
6.44 - val (model, where_) = Model_Pattern.parse ctxt model_input
6.45 + val (model, where_) = Model_Pattern.parse_pos ctxt model_input
6.46 + val (model', where_') = (map drop_pos_model model, map drop_pos_where_ where_)
6.47 val cas = CAS_Def.parse ctxt cas
6.48 val set_data =
6.49 ML_Context.expression (Input.pos_of source)
6.50 (ml "Theory.setup (Problem.set_data (" @ ML_Lex.read_source source @ ml "))")
6.51 |> Context.theory_map;
6.52 val where_rls = the_data (set_data thy);
6.53 - val arg = prep_store thy name maa id_empty
6.54 - (model, where_, cas) (pbl_id, met_ids, where_rls)
6.55 + val arg = prep_store thy name maa id_empty
6.56 + (model', where_', cas) (pbl_id, met_ids, where_rls)
6.57 in Know_Store.add_pbls ctxt [arg] thy end)))
6.58
6.59 in end;
7.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
7.2 +++ b/test/Tools/isac/BaseDefinitions/model-pattern.sml Thu Dec 15 13:03:51 2022 +0100
7.3 @@ -0,0 +1,75 @@
7.4 +(* Title: "BaseDefinition/model-pattern.sml"
7.5 + Author: Walther Neuper
7.6 +*)
7.7 +
7.8 +"-----------------------------------------------------------------------------------------------";
7.9 +"table of contents -----------------------------------------------------------------------------";
7.10 +"-----------------------------------------------------------------------------------------------";
7.11 +"----------- build fun Model_Pattern.parse_pos -----------------------------------------------------";
7.12 +"-----------------------------------------------------------------------------------------------";
7.13 +"-----------------------------------------------------------------------------------------------";
7.14 +"-----------------------------------------------------------------------------------------------";
7.15 +open Model_Pattern;
7.16 +
7.17 +"----------- build fun Model_Pattern.parse_pos -----------------------------------------------------";
7.18 +"----------- build fun Model_Pattern.parse_pos -----------------------------------------------------";
7.19 +"----------- build fun Model_Pattern.parse_pos -----------------------------------------------------";
7.20 +(*for problem pbl_equ_univ_lin : "LINEAR/univariate/equation"*)
7.21 +val input_to_Isar = (*vvvvvvvvvvvvv just for correct type *)
7.22 + [(*Given:*)
7.23 + ("equality e_e", Position.none),
7.24 + ("solveFor v_v", Position.none),
7.25 + (*Where:*)
7.26 + ("HOL.False", Position.none), (*for strange reasons*)
7.27 + ("Not( (lhs e_e) is_polyrat_in v_v)", Position.none),
7.28 + ("Not( (rhs e_e) is_polyrat_in v_v)", Position.none),
7.29 + ("((lhs e_e) has_degree_in v_v)=1", Position.none),
7.30 + ("((rhs e_e) has_degree_in v_v)=1", Position.none),
7.31 + (*Find:*)
7.32 + ("solutions v_v'i'", Position.none)]
7.33 +
7.34 +val model_input =
7.35 + [("#Given", (*-------------------------------vv=-3727*)
7.36 + [("<markup>", {offset=158, end_offset=172, id=3727}),
7.37 + ("<markup>", {offset=173, end_offset=187, id=3727})]),
7.38 + ("#Where",
7.39 + [("<markup>", {offset=197, end_offset=208, id=3727}),
7.40 + ("<markup>", {offset=269, end_offset=304, id=3727}),
7.41 + ("<markup>", {offset=309, end_offset=344, id=3727}),
7.42 + ("<markup>", {offset=349, end_offset=382, id=3727}),
7.43 + ("<markup>", {offset=386, end_offset=419, id=3727})]),
7.44 + ("#Find",
7.45 + [("<markup>", {offset=428, end_offset=446, id=3727})])]
7.46 +
7.47 +val model_input = (*type Position.T is hidden, thus redefinition*)
7.48 + [("#Given", (*-------------------------------vv=-3727*)
7.49 + [("equality e_e", Position.none),
7.50 + ("solveFor v_v", Position.none)]),
7.51 + ("#Where",
7.52 + [("HOL.False", Position.none),
7.53 + ("Not( (lhs e_e) is_polyrat_in v_v)", Position.none),
7.54 + ("Not( (rhs e_e) is_polyrat_in v_v)", Position.none),
7.55 + ("((lhs e_e) has_degree_in v_v)=1", Position.none),
7.56 + ("((rhs e_e) has_degree_in v_v)=1", Position.none)]),
7.57 + ("#Find",
7.58 + [("solutions v_v'i'", Position.none)])]: (m_field * (string * Position.T) list) list
7.59 +
7.60 +val thy = @{theory LinEq}
7.61 +val ctxt = Proof_Context.init_global thy;
7.62 +
7.63 +Model_Pattern.parse_pos ctxt model_input;
7.64 +"~~~~~ fun parse_pos , args:"; val (model_input) = (model_input);
7.65 + val items = model_input |> map (fn (m_field, items) => map (pair m_field) items) |> flat;
7.66 + val model = items
7.67 + |> filter_out ((fn f => (fn (f', _) => f = f')) "#Where")
7.68 + |> map (parse_term ctxt)
7.69 + |> map (split_descriptor ctxt)
7.70 +
7.71 +: Model_Pattern.pre_model
7.72 +
7.73 + val where_ = items
7.74 + |> filter ((fn f => (fn (f', _) => f = f')) "#Where")
7.75 + |> map (parse_pattern ctxt)
7.76 + |> map (fn (_, a, b) => (a, b))
7.77 +
7.78 +: (term * Position.T) list
8.1 --- a/test/Tools/isac/Knowledge/build_thydata.sml Fri Dec 09 16:29:04 2022 +0100
8.2 +++ b/test/Tools/isac/Knowledge/build_thydata.sml Thu Dec 15 13:03:51 2022 +0100
8.3 @@ -16,11 +16,14 @@
8.4 "-----------------------------------------------------------------";
8.5 "-----------------------------------------------------------------";
8.6 "-----------------------------------------------------------------";
8.7 +val thy = @{theory Build_Thydata}
8.8 +val ctxt = Proof_Context.init_global thy;
8.9
8.10 "----------- retrieve errpats ------------------------------------";
8.11 "----------- retrieve errpats ------------------------------------";
8.12 "----------- retrieve errpats ------------------------------------";
8.13 -val {errpats, rew_rls, program = Prog prog, ...} = MethodC.from_store ctxt ["diff", "differentiate_on_R"];
8.14 +val {errpats, rew_rls, program = Prog prog, ...} =
8.15 + MethodC.from_store ctxt ["diff", "differentiate_on_R"];
8.16 case errpats of [("chain-rule-diff-both", _, _)] => ()
8.17 | _ => error "errpats chain-rule-diff-both changed"
8.18
9.1 --- a/test/Tools/isac/Knowledge/integrate.thy Fri Dec 09 16:29:04 2022 +0100
9.2 +++ b/test/Tools/isac/Knowledge/integrate.thy Thu Dec 15 13:03:51 2022 +0100
9.3 @@ -15,19 +15,24 @@
9.4 (Rewrite_Set_Inst [(''bdv'',v_v)] ''add_new_c'') #>
9.5 (Rewrite_Set_Inst [(''bdv'',v_v)] ''simplify_Integral'')) (f_f::real))"
9.6 ML \<open>
9.7 +(*/----- local in struct Problem -------------\*)
9.8 +val drop_pos_model = (fn (a, b, _) => (a, b))
9.9 +val drop_pos_where_ = (fn (b, _) => b)
9.10 +(*\----- local in struct Problem -------------/*)
9.11 val model_input = [("#Given", [("functionTerm f_f", Position.none),
9.12 ("integrateBy v_v", Position.none)]),
9.13 ("#Find", [("antiDerivative F_F", Position.none)])]
9.14 (* cp from method.sml, Outer_Syntax.command \<^command_keyword>\<open>method\<close> *)
9.15 val thy = @{theory}
9.16 val ctxt = Proof_Context.init_global thy
9.17 - val (model, where_) = Model_Pattern.parse ctxt model_input
9.18 + val (model, where_) = Model_Pattern.parse_pos ctxt model_input
9.19 + val (model', where_') = (map drop_pos_model model, map drop_pos_where_ where_)
9.20 val ml_input =
9.21 {rew_ord = "sqrt_right", rls'= tval_rls, prog_rls = Rule_Set.empty, where_rls = Rule_Set.empty,
9.22 calc = [], errpats = [], rew_rls = Rule_Set.empty} : MethodC.ml_input
9.23 val thm = @{thm integration_test.simps}
9.24 val arg = MethodC.prep_store thy "met_testint" [] Problem.id_empty
9.25 - (["diff", "integration", "test"], model, where_, ml_input, thm)
9.26 + (["diff", "integration", "test"], model', where_', ml_input, thm)
9.27 \<close>
9.28 setup \<open>Know_Store.add_mets @{context} [arg]\<close>
9.29
10.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
10.2 +++ b/test/Tools/isac/MathEngBasic/problem.sml Thu Dec 15 13:03:51 2022 +0100
10.3 @@ -0,0 +1,51 @@
10.4 +(* Title: "MathengineBasic/problem.sml"
10.5 + Author: Walther Neuper
10.6 +*)
10.7 +
10.8 +"-----------------------------------------------------------------------------------------------";
10.9 +"table of contents -----------------------------------------------------------------------------";
10.10 +"-----------------------------------------------------------------------------------------------";
10.11 +"----------- rebuild fun Outer_Syntax.command \<^command_keyword>\<open>problem\<close> ------------------------";
10.12 +"-----------------------------------------------------------------------------------------------";
10.13 +"-----------------------------------------------------------------------------------------------";
10.14 +"-----------------------------------------------------------------------------------------------";
10.15 +
10.16 +"----------- rebuild fun Outer_Syntax.command \<^command_keyword>\<open>problem\<close> ------------------------";
10.17 +"----------- rebuild fun Outer_Syntax.command \<^command_keyword>\<open>problem\<close> ------------------------";
10.18 +"----------- rebuild fun Outer_Syntax.command \<^command_keyword>\<open>problem\<close> ------------------------";
10.19 +val drop_pos_model = (fn (a, b, _) => (a, b))
10.20 +val drop_pos_where_ = (fn (b, _) => b);
10.21 +
10.22 +"~~~~~ fun Outer_Syntax.command \<^command_keyword>\<open>problem\<close> , args:"; val () = ();
10.23 +(*for problem pbl_equ_univ_lin : "LINEAR/univariate/equation"*)
10.24 +val thy = @{theory LinEq}
10.25 +val ctxt = Proof_Context.init_global thy;
10.26 +val model_input = (*type Position.T is hidden, thus redefinition*)
10.27 + [("#Given", (*-------------------------------vv=-3727*)
10.28 + [("equality e_e", Position.none),
10.29 + ("solveFor v_v", Position.none)]),
10.30 + ("#Where",
10.31 + [("HOL.False", Position.none),
10.32 + ("Not( (lhs e_e) is_polyrat_in v_v)", Position.none),
10.33 + ("Not( (rhs e_e) is_polyrat_in v_v)", Position.none),
10.34 + ("((lhs e_e) has_degree_in v_v)=1", Position.none),
10.35 + ("((rhs e_e) has_degree_in v_v)=1", Position.none)]),
10.36 + ("#Find",
10.37 + [("solutions v_v'i'", Position.none)])]: (Model_Pattern.m_field * (string * Position.T) list) list
10.38 +
10.39 + val (model, where_) = Model_Pattern.parse_pos ctxt model_input;
10.40 +
10.41 +(* ARGUMENTS DEFINED BELOW:
10.42 + prep_store thy name maa id_empty
10.43 + (model, where_, cas) (pbl_id, met_ids, where_rls); *)
10.44 +"~~~~~ fun prep_store , args:"; val (thy, name, maa, start_refine,
10.45 + (model, where_, cas), (pbl_id, met_ids, where_rls)) =
10.46 + (@{theory LinEq}, "pbl_equ_univ_lin", [""], Problem.id_empty,
10.47 + (model, where_, NONE: term option), (Problem.id_empty, [MethodC.id_empty], Rule_Set.empty));
10.48 +(*for problem pbl_equ_univ_lin : "LINEAR/univariate/equation"*)
10.49 +
10.50 + val (model, where_) = Model_Pattern.parse_pos ctxt model_input
10.51 + val (model', where_') = (map drop_pos_model model, map drop_pos_where_ where_)
10.52 +
10.53 + val arg = Problem.prep_store thy name maa Problem.id_empty
10.54 + (model', where_', cas) (pbl_id, met_ids, where_rls)
11.1 --- a/test/Tools/isac/ProgLang/calculate.thy Fri Dec 09 16:29:04 2022 +0100
11.2 +++ b/test/Tools/isac/ProgLang/calculate.thy Thu Dec 15 13:03:51 2022 +0100
11.3 @@ -11,6 +11,10 @@
11.4 *setup* Know_Store.add_pbls / add_mets is impossible in *.sml files.
11.5 The respective test/../evaluate.sml is called in Test_Isac.thy.
11.6 \<close> ML \<open>
11.7 +(*/----- local in struct Problem -------------\*)
11.8 +val drop_pos_model = (fn (a, b, _) => (a, b))
11.9 +val drop_pos_where_ = (fn (b, _) => b)
11.10 +(*\----- local in struct Problem -------------/*)
11.11 val thy = @{theory "Test"}
11.12 val arg_1 = Problem.prep_store thy "pbl_ttest" [] Problem.id_empty
11.13 ([], [], NONE) (["test"], [], Rule_Set.empty)
11.14 @@ -19,9 +23,10 @@
11.15 ("#Find", [("realTestFind s_s", Position.none)])]
11.16 (* cp from problem.sml, Outer_Syntax.command \<^command_keyword>\<open>problem\<close> *)
11.17 val ctxt = Proof_Context.init_global thy
11.18 - val (model, where_) = Model_Pattern.parse ctxt model_input
11.19 + val (model, where_) = Model_Pattern.parse_pos ctxt model_input
11.20 + val (model', where_') = (map drop_pos_model model, map drop_pos_where_ where_)
11.21 val arg_2 = Problem.prep_store thy "pbl_ttest_calc" [] Problem.id_empty
11.22 - (model, where_, NONE)
11.23 + (model', where_', NONE)
11.24 (["calculate", "test"], [["Test", "test_calculate"]], Rule_Set.empty)
11.25 \<close>
11.26 setup \<open>Know_Store.add_pbls @{context} [arg_1, arg_2]\<close>
11.27 @@ -39,7 +44,8 @@
11.28 val model_input = [("#Given", [("realTestGiven t_t", Position.none)]),
11.29 ("#Find", [("realTestFind s_s", Position.none)])]
11.30 (* cp from method.sml, Outer_Syntax.command \<^command_keyword>\<open>method\<close> *)
11.31 - val (model, where_) = Model_Pattern.parse ctxt model_input
11.32 + val (model, where_) = Model_Pattern.parse_pos ctxt model_input
11.33 + val (model', where_') = (map drop_pos_model model, map drop_pos_where_ where_)
11.34 val ml_input =
11.35 {rew_ord = "sqrt_right", rls'= tval_rls, prog_rls = Rule_Set.empty, where_rls = Rule_Set.empty,
11.36 calc = [("PLUS", (\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_")),
11.37 @@ -49,7 +55,7 @@
11.38 errpats = [], rew_rls = Rule_Set.empty} : MethodC.ml_input
11.39 val thm = @{thm calc_test.simps}
11.40 val arg = MethodC.prep_store thy "met_testcal" [] Problem.id_empty
11.41 - (["Test", "test_calculate"], model, where_, ml_input, thm)
11.42 + (["Test", "test_calculate"], model', where_', ml_input, thm)
11.43 \<close>
11.44 setup \<open>Know_Store.add_mets @{context} [arg]
11.45 \<close>
12.1 --- a/test/Tools/isac/Specify/refine.thy Fri Dec 09 16:29:04 2022 +0100
12.2 +++ b/test/Tools/isac/Specify/refine.thy Thu Dec 15 13:03:51 2022 +0100
12.3 @@ -12,55 +12,63 @@
12.4 *setup* Know_Store.add_pbls is impossible in *.sml files.
12.5 The respective test/../refine.sml is called in Test_Isac.thy.
12.6 \<close> ML \<open>
12.7 +(*/----- local in struct Problem -------------\*)
12.8 +val drop_pos_model = (fn (a, b, _) => (a, b))
12.9 +val drop_pos_where_ = (fn (b, _) => b)
12.10 +(*\----- local in struct Problem -------------/*)
12.11 val thy = @{theory "Test"}
12.12 \<close> ML \<open>
12.13 (* cp from problem.sml, Outer_Syntax.command \<^command_keyword>\<open>problem\<close> *)
12.14 val arg_1 = Problem.prep_store thy "pbl_test_refine" [] Problem.id_empty
12.15 ([], [], NONE) (["refine", "test"], [], Rule_Set.empty)
12.16
12.17 - val (model, where_) = Model_Pattern.parse ctxt
12.18 + val (model, where_) = Model_Pattern.parse_pos ctxt
12.19 [("#Given", [("fixedValues a_a", Position.none)])]
12.20 + val (model', where_') = (map drop_pos_model model, map drop_pos_where_ where_)
12.21 val arg_2 = Problem.prep_store thy "pbl_pbla" [] Problem.id_empty
12.22 - (model, where_, NONE) (["pbla", "refine", "test"], [], Rule_Set.empty)
12.23 + (model', where_', NONE) (["pbla", "refine", "test"], [], Rule_Set.empty)
12.24
12.25 - val (model, where_) = Model_Pattern.parse ctxt
12.26 - [("#Given", [("fixedValues a_a", Position.none),
12.27 - ("maximum a_1", Position.none)])]
12.28 + val (model, where_) = Model_Pattern.parse_pos ctxt
12.29 + [("#Given", [("fixedValues a_a", Position.none), ("maximum a_1", Position.none)])]
12.30 + val (model', where_') = (map drop_pos_model model, map drop_pos_where_ where_)
12.31 val arg_3 = Problem.prep_store thy "pbl_pbla1" [] Problem.id_empty
12.32 - (model, where_, NONE) (["pbla1", "pbla", "refine", "test"], [], Rule_Set.empty)
12.33 + (model', where_', NONE) (["pbla1", "pbla", "refine", "test"], [], Rule_Set.empty)
12.34
12.35 - val (model, where_) = Model_Pattern.parse ctxt
12.36 - [("#Given", [("fixedValues a_a", Position.none),
12.37 - ("valuesFor a_2", Position.none)])]
12.38 + val (model, where_) = Model_Pattern.parse_pos ctxt
12.39 + [("#Given", [("fixedValues a_a", Position.none), ("valuesFor a_2", Position.none)])]
12.40 + val (model', where_') = (map drop_pos_model model, map drop_pos_where_ where_)
12.41 val arg_4 = Problem.prep_store thy "pbl_pbla2" [] Problem.id_empty
12.42 - (model, where_, NONE) (["pbla2", "pbla", "refine", "test"], [], Rule_Set.empty)
12.43 + (model', where_', NONE) (["pbla2", "pbla", "refine", "test"], [], Rule_Set.empty)
12.44
12.45 - val (model, where_) = Model_Pattern.parse ctxt
12.46 + val (model, where_) = Model_Pattern.parse_pos ctxt
12.47 [("#Given", [("fixedValues a_a", Position.none),
12.48 ("valuesFor a_2", Position.none),
12.49 ("functionOf a2_x", Position.none)])]
12.50 + val (model', where_') = (map drop_pos_model model, map drop_pos_where_ where_)
12.51 val arg_5 = Problem.prep_store thy "pbl_pbla2x" [] Problem.id_empty
12.52 - (model, where_, NONE) (["pbla2x", "pbla2", "pbla", "refine", "test"], [], Rule_Set.empty)
12.53 + (model', where_', NONE) (["pbla2x", "pbla2", "pbla", "refine", "test"], [], Rule_Set.empty)
12.54
12.55 - val (model, where_) = Model_Pattern.parse ctxt
12.56 + val (model, where_) = Model_Pattern.parse_pos ctxt
12.57 [("#Given", [("fixedValues a_a", Position.none),
12.58 ("valuesFor a_2", Position.none),
12.59 ("boundVariable a2_y", Position.none)])]
12.60 + val (model', where_') = (map drop_pos_model model, map drop_pos_where_ where_)
12.61 val arg_6 = Problem.prep_store thy "pbl_pbla2y" [] Problem.id_empty
12.62 - (model, where_, NONE) (["pbla2y", "pbla2", "pbla", "refine", "test"], [], Rule_Set.empty)
12.63 + (model', where_', NONE) (["pbla2y", "pbla2", "pbla", "refine", "test"], [], Rule_Set.empty)
12.64
12.65 - val (model, where_) = Model_Pattern.parse ctxt
12.66 + val (model, where_) = Model_Pattern.parse_pos ctxt
12.67 [("#Given", [("fixedValues a_a", Position.none),
12.68 ("valuesFor a_2", Position.none),
12.69 ("interval a2_z", Position.none)])]
12.70 val arg_7 = Problem.prep_store thy "pbl_pbla2z" [] Problem.id_empty
12.71 - (model, where_, NONE) (["pbla2z", "pbla2", "pbla", "refine", "test"], [], Rule_Set.empty)
12.72 + (model', where_', NONE) (["pbla2z", "pbla2", "pbla", "refine", "test"], [], Rule_Set.empty)
12.73
12.74 - val (model, where_) = Model_Pattern.parse ctxt
12.75 + val (model, where_) = Model_Pattern.parse_pos ctxt
12.76 [("#Given", [("fixedValues a_a", Position.none),
12.77 ("relations a_3", Position.none)])]
12.78 + val (model', where_') = (map drop_pos_model model, map drop_pos_where_ where_)
12.79 val arg_8 = Problem.prep_store thy "pbl_pbla3" [] Problem.id_empty
12.80 - (model, where_, NONE) (["pbla3", "pbla", "refine", "test"], [], Rule_Set.empty)
12.81 + (model', where_', NONE) (["pbla3", "pbla", "refine", "test"], [], Rule_Set.empty)
12.82 \<close>
12.83 setup \<open>Know_Store.add_pbls @{context} [arg_1, arg_2, arg_3, arg_4, arg_5, arg_6, arg_7, arg_8]\<close>
12.84
13.1 --- a/test/Tools/isac/Test_Isac.thy Fri Dec 09 16:29:04 2022 +0100
13.2 +++ b/test/Tools/isac/Test_Isac.thy Thu Dec 15 13:03:51 2022 +0100
13.3 @@ -82,6 +82,7 @@
13.4 "$ISABELLE_ISAC/Knowledge/GCD_Poly_FP" (*not imported by Isac.thy*) (*Test_Isac_Short*)
13.5 (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)
13.6 (**)
13.7 + "$ISABELLE_ISAC_TEST/Tools/isac/BridgeJEdit/Test_VSCode_Example"
13.8
13.9 begin
13.10
13.11 @@ -209,6 +210,7 @@
13.12 ML_file "BaseDefinitions/theoryC.sml"
13.13 ML_file "BaseDefinitions/rule.sml"
13.14 ML_file "BaseDefinitions/thmC-def.sml"
13.15 + ML_file "BaseDefinitions/model-pattern.sml"
13.16 ML_file "BaseDefinitions/error-fill-def.sml"
13.17 ML_file "BaseDefinitions/rule-set.sml"
13.18 ML_file "BaseDefinitions/check-unique.sml"
13.19 @@ -259,9 +261,10 @@
13.20
13.21 subsection \<open>further functionality alongside batch build sequence\<close>
13.22 ML_file "MathEngBasic/thmC.sml"
13.23 + ML_file "MathEngBasic/problem.sml"
13.24 ML_file "MathEngBasic/rewrite.sml"
13.25 ML_file "MathEngBasic/tactic.sml"
13.26 - ML_file "MathEngBasic/ctree.sml"
13.27 + ML_file "MathEngBasic/ctree.sml" (*if red, get the file into a text buffer -- this might clear*)
13.28 ML_file "MathEngBasic/calculation.sml"
13.29
13.30 ML_file "Specify/formalise.sml"
13.31 @@ -300,6 +303,7 @@
13.32 ML_file "BridgeLibisabelle/thy-hierarchy.sml"
13.33 ML_file "BridgeLibisabelle/interface-xml.sml" (*TODO after 2009-2*)
13.34 ML_file "BridgeLibisabelle/interface.sml"
13.35 +
13.36 ML_file "BridgeJEdit/parseC.sml"
13.37 ML_file "BridgeJEdit/preliminary.sml"
13.38 ML_file "BridgeJEdit/vscode-example.sml"
14.1 --- a/test/Tools/isac/Test_Isac_Short.thy Fri Dec 09 16:29:04 2022 +0100
14.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Thu Dec 15 13:03:51 2022 +0100
14.3 @@ -206,10 +206,11 @@
14.4 ML_file "BaseDefinitions/libraryC.sml"
14.5 ML_file "BaseDefinitions/rule-def.sml"
14.6 ML_file "BaseDefinitions/eval-def.sml"
14.7 - ML_file "BaseDefinitions/rewrite-order.sml"
14.8 + ML_file "BaseDefinitions/rewrite-order.sml"
14.9 ML_file "BaseDefinitions/theoryC.sml"
14.10 ML_file "BaseDefinitions/rule.sml"
14.11 ML_file "BaseDefinitions/thmC-def.sml"
14.12 + ML_file "BaseDefinitions/model-pattern.sml"
14.13 ML_file "BaseDefinitions/error-fill-def.sml"
14.14 ML_file "BaseDefinitions/rule-set.sml"
14.15 ML_file "BaseDefinitions/check-unique.sml"
14.16 @@ -260,6 +261,7 @@
14.17
14.18 subsection \<open>further functionality alongside batch build sequence\<close>
14.19 ML_file "MathEngBasic/thmC.sml"
14.20 + ML_file "MathEngBasic/problem.sml"
14.21 ML_file "MathEngBasic/rewrite.sml"
14.22 ML_file "MathEngBasic/tactic.sml"
14.23 ML_file "MathEngBasic/ctree.sml" (*if red, get the file into a text buffer -- this might clear*)
14.24 @@ -291,7 +293,7 @@
14.25 ML_file "MathEngine/fetch-tactics.sml"
14.26 ML_file "MathEngine/solve.sml"
14.27 ML_file "MathEngine/step.sml"
14.28 - ML_file "MathEngine/mathengine-stateless.sml" (*!part. WN130804: +check Interpret/me.sml*)
14.29 + ML_file "MathEngine/mathengine-stateless.sml"
14.30 ML_file "MathEngine/messages.sml"
14.31 ML_file "MathEngine/states.sml"
14.32
14.33 @@ -334,7 +336,7 @@
14.34 ML_file "Knowledge/eqsystem-1a.sml"
14.35 ML_file "Knowledge/eqsystem-2.sml"
14.36 ML_file "Knowledge/test.sml"
14.37 - ML_file "Knowledge/polyminus.sml"
14.38 + ML_file "Knowledge/polyminus.sml"
14.39 ML_file "Knowledge/vect.sml"
14.40 ML_file "Knowledge/diff-app.sml" (* postponed to dev. specification | TP-prog. *)
14.41 ML_file "Knowledge/biegelinie-1.sml"