1.1 --- a/src/Tools/isac/Build_Isac.thy Mon Dec 31 14:15:19 2018 +0100
1.2 +++ b/src/Tools/isac/Build_Isac.thy Mon Dec 31 14:49:16 2018 +0100
1.3 @@ -74,36 +74,6 @@
1.4 ML \<open>
1.5 \<close> ML \<open>
1.6 \<close>
1.7 -
1.8 -(*==============================================================================================
1.9 - The test below from calculate.sml raises an exception with the cleaned Rewrite.
1.10 - The differences to the working 'fun rewrite' are that significant,
1.11 - that we want to rely on 'hg revert'.
1.12 - For that purpose we save this changeset with a broken 'fun rewrite' and tests not running.
1.13 -*)
1.14 -ML \<open>
1.15 -\<close> ML \<open>
1.16 -(*--------------(2): does divide work in Test_simplify ?: ------*)
1.17 - val thy = @{theory Test};
1.18 - val t = (Thm.term_of o the o (TermC.parse thy)) "6 / 2";
1.19 - val rls = Test_simplify;
1.20 -\<close> ML \<open>
1.21 - val (t,_) = the (Rewrite.rewrite_set_ thy false rls t);
1.22 -(*val t = Free ("3","Real.real") : term*)
1.23 -\<close> ML \<open>
1.24 -
1.25 -(*--------------(3): is_const works ?: -------------------------------------*)
1.26 - val t = (Thm.term_of o the o (TermC.parse @{theory})) "2 is_const";
1.27 -\<close> ML \<open>
1.28 - Rewrite.rewrite_set_ @{theory Test} false tval_rls t;
1.29 -
1.30 -(* exception TERM raised (line 270 of "~~/src/HOL/Tools/hologic.ML"):
1.31 - dest_eq
1.32 - 0 \<le> ?a \<Longrightarrow> (0 \<le> sqrt ?a) = True*)
1.33 -\<close> ML \<open>
1.34 -\<close>
1.35 -(*==============================================================================================*)
1.36 -
1.37 ML \<open>Calc.adhoc_thm; (*from "ProgLang/calculate.sml" *)\<close>
1.38 ML \<open>Rewrite.rewrite_; (*from "ProgLang/rewrite.sml" *)\<close>
1.39 ML \<open>LTool.is_reall_dsc; (*from "ProgLang/scrtools.sml" *)\<close>
2.1 --- a/src/Tools/isac/Interpret/appl.sml Mon Dec 31 14:15:19 2018 +0100
2.2 +++ b/src/Tools/isac/Interpret/appl.sml Mon Dec 31 14:49:16 2018 +0100
2.3 @@ -505,7 +505,7 @@
2.4 Frm => get_obj g_form pt p
2.5 | Res => (fst o (get_obj g_result pt)) p
2.6 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
2.7 - in (let val ls = or2list f
2.8 + in (let val ls = Tools.or2list f
2.9 in Chead.Appl (Tac.Or_to_List' (f, ls)) end)
2.10 handle _ => Chead.Notappl ("'Or_to_List' not applicable to " ^ Rule.term2str f)
2.11 end
3.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy Mon Dec 31 14:15:19 2018 +0100
3.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy Mon Dec 31 14:49:16 2018 +0100
3.3 @@ -149,8 +149,8 @@
3.4 rules = [Rule.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}),
3.5 Rule.Calc("Groups.plus_class.plus", eval_binop "#add_"),
3.6 Rule.Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL}),
3.7 - Rule.Calc("Tools.lhs", eval_lhs"eval_lhs_"),
3.8 - Rule.Calc("Tools.rhs", eval_rhs"eval_rhs_"),
3.9 + Rule.Calc("Tools.lhs", Tools.eval_lhs"eval_lhs_"),
3.10 + Rule.Calc("Tools.rhs", Tools.eval_rhs"eval_rhs_"),
3.11 Rule.Calc("Atools.argument'_in",
3.12 eval_argument_in "Atools.argument'_in")
3.13 ],
3.14 @@ -170,7 +170,7 @@
3.15 rules = [Rule.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}),
3.16 Rule.Calc("Groups.plus_class.plus", eval_binop "#add_"),
3.17 Rule.Thm ("NTH_NIL", TermC.num_str @{thm NTH_NIL}),
3.18 - Rule.Calc("Tools.lhs", eval_lhs "eval_lhs_"),
3.19 + Rule.Calc("Tools.lhs", Tools.eval_lhs "eval_lhs_"),
3.20 Rule.Calc("Atools.filter'_sameFunId",
3.21 eval_filter_sameFunId "Atools.filter'_sameFunId"),
3.22 (*WN070514 just for smltest/../biegelinie.sml ...*)
3.23 @@ -310,7 +310,7 @@
3.24 Rule.Thm ("not_false",TermC.num_str @{thm not_false})],
3.25 calc = [],
3.26 srls = Rule.append_rls "erls_IntegrierenUndK.." Rule.e_rls
3.27 - [Rule.Calc("Tools.rhs", eval_rhs"eval_rhs_"),
3.28 + [Rule.Calc("Tools.rhs", Tools.eval_rhs"eval_rhs_"),
3.29 Rule.Calc ("Atools.ident",eval_ident "#ident_"),
3.30 Rule.Thm ("last_thmI",TermC.num_str @{thm last_thmI}),
3.31 Rule.Thm ("if_True",TermC.num_str @{thm if_True}),
3.32 @@ -369,7 +369,7 @@
3.33 Rule.Thm ("not_false", TermC.num_str @{thm not_false})],
3.34 calc = [],
3.35 srls = Rule.append_rls "srls_ausBelastung" Rule.e_rls
3.36 - [Rule.Calc ("Tools.rhs", eval_rhs "eval_rhs_")],
3.37 + [Rule.Calc ("Tools.rhs", Tools.eval_rhs "eval_rhs_")],
3.38 prls = Rule.e_rls, crls = Atools_erls, errpats = [], nrls = Rule.e_rls},
3.39 "Script Belastung2BiegelScript (q__q::real) (v_v::real) = " ^
3.40 " (let q___q = Take (qq v_v = q__q); " ^
3.41 @@ -468,7 +468,7 @@
3.42 ("#Find" ,["equality equ'''"])],
3.43 {rew_ord'="tless_true", rls'=Rule.Erls, calc = [],
3.44 srls = Rule.append_rls "srls_in_EquationfromFunc" Rule.e_rls
3.45 - [Rule.Calc("Tools.lhs", eval_lhs"eval_lhs_"),
3.46 + [Rule.Calc("Tools.lhs", Tools.eval_lhs "eval_lhs_"),
3.47 Rule.Calc("Atools.argument'_in", eval_argument_in "Atools.argument'_in")],
3.48 prls=Rule.e_rls, crls = Atools_erls, errpats = [], nrls = Rule.e_rls},
3.49 (*(M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) (M_b L = 0) -->
4.1 --- a/src/Tools/isac/Knowledge/Diff.thy Mon Dec 31 14:15:19 2018 +0100
4.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Mon Dec 31 14:49:16 2018 +0100
4.3 @@ -183,8 +183,8 @@
4.4 rew_ord = ("termlessI",termlessI),
4.5 erls = Rule.e_rls,
4.6 srls = Rule.Erls, calc = [], errpatts = [],
4.7 - rules = [Rule.Calc("Tools.lhs", eval_lhs "eval_lhs_"),
4.8 - Rule.Calc("Tools.rhs", eval_rhs "eval_rhs_"),
4.9 + rules = [Rule.Calc("Tools.lhs", Tools.eval_lhs "eval_lhs_"),
4.10 + Rule.Calc("Tools.rhs", Tools.eval_rhs "eval_rhs_"),
4.11 Rule.Calc("Diff.primed", eval_primed "Diff.primed")
4.12 ],
4.13 scr = Rule.EmptyScr};
5.1 --- a/src/Tools/isac/Knowledge/DiffApp.thy Mon Dec 31 14:15:19 2018 +0100
5.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy Mon Dec 31 14:49:16 2018 +0100
5.3 @@ -69,7 +69,7 @@
5.4 Rule.Calc ("Atools.ident", eval_ident "#ident_"),
5.5 Rule.Calc ("Atools.is'_const", eval_const "#is_const_"),
5.6 Rule.Calc ("Atools.occurs'_in", eval_occurs_in ""),
5.7 - Rule.Calc ("Tools.matches", eval_matches "")],
5.8 + Rule.Calc ("Tools.matches", Tools.eval_matches "")],
5.9 scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
5.10 });
5.11 \<close>
6.1 --- a/src/Tools/isac/Knowledge/Equation.thy Mon Dec 31 14:15:19 2018 +0100
6.2 +++ b/src/Tools/isac/Knowledge/Equation.thy Mon Dec 31 14:49:16 2018 +0100
6.3 @@ -43,7 +43,7 @@
6.4
6.5 val univariate_equation_prls =
6.6 Rule.append_rls "univariate_equation_prls" Rule.e_rls
6.7 - [Rule.Calc ("Tools.matches",eval_matches "")];
6.8 + [Rule.Calc ("Tools.matches", Tools.eval_matches "")];
6.9 \<close>
6.10 setup \<open>KEStore_Elems.add_rlss [("univariate_equation_prls",
6.11 (Context.theory_name @{theory}, LTool.prep_rls @{theory} univariate_equation_prls))]\<close>
6.12 @@ -53,7 +53,7 @@
6.13 [("#Given" ,["equality e_e","solveFor v_v"]),
6.14 ("#Where" ,["matches (?a = ?b) e_e"]),
6.15 ("#Find" ,["solutions v_v'i'"])],
6.16 - Rule.append_rls "equation_prls" Rule.e_rls [Rule.Calc ("Tools.matches",eval_matches "")],
6.17 + Rule.append_rls "equation_prls" Rule.e_rls [Rule.Calc ("Tools.matches", Tools.eval_matches "")],
6.18 SOME "solve (e_e::bool, v_v)", [])),
6.19 (Specify.prep_pbt thy "pbl_equ_univ" [] Celem.e_pblID
6.20 (["univariate","equation"],
7.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Mon Dec 31 14:15:19 2018 +0100
7.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Mon Dec 31 14:49:16 2018 +0100
7.3 @@ -150,7 +150,7 @@
7.4 rew_ord = ("termlessI",termlessI),
7.5 erls = Rule.Erls,
7.6 srls = Rule.Erls, calc = [], errpatts = [],
7.7 - rules = [Rule.Calc ("Tools.matches", eval_matches""),
7.8 + rules = [Rule.Calc ("Tools.matches", Tools.eval_matches""),
7.9 Rule.Calc ("Integrate.is'_f'_x",
7.10 eval_is_f_x "is_f_x_"),
7.11 Rule.Thm ("not_true", TermC.num_str @{thm not_true}),
8.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Mon Dec 31 14:15:19 2018 +0100
8.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Mon Dec 31 14:49:16 2018 +0100
8.3 @@ -197,8 +197,8 @@
8.4 rules = [Rule.Thm ("NTH_CONS", @{thm NTH_CONS}),
8.5 Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
8.6 Rule.Thm ("NTH_NIL", @{thm NTH_NIL}),
8.7 - Rule.Calc ("Tools.lhs", eval_lhs "eval_lhs_"),
8.8 - Rule.Calc ("Tools.rhs", eval_rhs"eval_rhs_"),
8.9 + Rule.Calc ("Tools.lhs", Tools.eval_lhs "eval_lhs_"),
8.10 + Rule.Calc ("Tools.rhs", Tools.eval_rhs"eval_rhs_"),
8.11 Rule.Calc ("Atools.argument'_in", eval_argument_in "Atools.argument'_in"),
8.12 Rule.Calc ("Rational.get_denominator", eval_get_denominator "#get_denominator"),
8.13 Rule.Calc ("Rational.get_numerator", eval_get_numerator "#get_numerator"),
9.1 --- a/src/Tools/isac/Knowledge/LinEq.thy Mon Dec 31 14:15:19 2018 +0100
9.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Mon Dec 31 14:49:16 2018 +0100
9.3 @@ -34,9 +34,9 @@
9.4 val LinEq_prls = (*3.10.02:just the following order due to subterm evaluation*)
9.5 Rule.append_rls "LinEq_prls" Rule.e_rls
9.6 [Rule.Calc ("HOL.eq",eval_equal "#equal_"),
9.7 - Rule.Calc ("Tools.matches",eval_matches ""),
9.8 - Rule.Calc ("Tools.lhs" ,eval_lhs ""),
9.9 - Rule.Calc ("Tools.rhs" ,eval_rhs ""),
9.10 + Rule.Calc ("Tools.matches", Tools.eval_matches ""),
9.11 + Rule.Calc ("Tools.lhs" , Tools.eval_lhs ""),
9.12 + Rule.Calc ("Tools.rhs" , Tools.eval_rhs ""),
9.13 Rule.Calc ("Poly.has'_degree'_in",eval_has_degree_in ""),
9.14 Rule.Calc ("Poly.is'_polyrat'_in",eval_is_polyrat_in ""),
9.15 Rule.Calc ("Atools.occurs'_in",eval_occurs_in ""),
10.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy Mon Dec 31 14:15:19 2018 +0100
10.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy Mon Dec 31 14:49:16 2018 +0100
10.3 @@ -199,8 +199,8 @@
10.4 Rule.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}),
10.5 Rule.Calc("Groups.plus_class.plus", eval_binop "#add_"),
10.6 Rule.Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL}),
10.7 - Rule.Calc("Tools.lhs", eval_lhs "eval_lhs_"),
10.8 - Rule.Calc("Tools.rhs", eval_rhs"eval_rhs_"),
10.9 + Rule.Calc("Tools.lhs", Tools.eval_lhs "eval_lhs_"),
10.10 + Rule.Calc("Tools.rhs", Tools.eval_rhs"eval_rhs_"),
10.11 Rule.Calc("Atools.argument'_in", eval_argument_in "Atools.argument'_in"),
10.12 Rule.Calc("Rational.get_denominator", eval_get_denominator "#get_denominator"),
10.13 Rule.Calc("Rational.get_numerator", eval_get_numerator "#get_numerator"),
11.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Mon Dec 31 14:15:19 2018 +0100
11.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Mon Dec 31 14:49:16 2018 +0100
11.3 @@ -378,9 +378,9 @@
11.4 val PolyEq_prls = (*3.10.02:just the following order due to subterm evaluation*)
11.5 Rule.append_rls "PolyEq_prls" Rule.e_rls
11.6 [Rule.Calc ("Atools.ident",eval_ident "#ident_"),
11.7 - Rule.Calc ("Tools.matches",eval_matches ""),
11.8 - Rule.Calc ("Tools.lhs" ,eval_lhs ""),
11.9 - Rule.Calc ("Tools.rhs" ,eval_rhs ""),
11.10 + Rule.Calc ("Tools.matches", Tools.eval_matches ""),
11.11 + Rule.Calc ("Tools.lhs" , Tools.eval_lhs ""),
11.12 + Rule.Calc ("Tools.rhs" , Tools.eval_rhs ""),
11.13 Rule.Calc ("Poly.is'_expanded'_in",eval_is_expanded_in ""),
11.14 Rule.Calc ("Poly.is'_poly'_in",eval_is_poly_in ""),
11.15 Rule.Calc ("Poly.has'_degree'_in",eval_has_degree_in ""),
12.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy Mon Dec 31 14:15:19 2018 +0100
12.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy Mon Dec 31 14:49:16 2018 +0100
12.3 @@ -414,7 +414,7 @@
12.4 ("#Find", ["normalform n_n"])],
12.5 Rule.append_rls "prls_pbl_vereinf_poly" Rule.e_rls
12.6 [Rule.Calc ("Poly.is'_polyexp", eval_is_polyexp ""),
12.7 - Rule.Calc ("Tools.matchsub", eval_matchsub ""),
12.8 + Rule.Calc ("Tools.matchsub", Tools.eval_matchsub ""),
12.9 Rule.Thm ("or_true", TermC.num_str @{thm or_true}),
12.10 (*"(?a | True) = True"*)
12.11 Rule.Thm ("or_false", TermC.num_str @{thm or_false}),
12.12 @@ -435,7 +435,7 @@
12.13 ("#Find" ,["normalform n_n"])],
12.14 Rule.append_rls "prls_pbl_vereinf_poly_klammer" Rule.e_rls
12.15 [Rule.Calc ("Poly.is'_polyexp", eval_is_polyexp ""),
12.16 - Rule.Calc ("Tools.matchsub", eval_matchsub ""),
12.17 + Rule.Calc ("Tools.matchsub", Tools.eval_matchsub ""),
12.18 Rule.Thm ("or_true", TermC.num_str @{thm or_true}),
12.19 (*"(?a | True) = True"*)
12.20 Rule.Thm ("or_false", TermC.num_str @{thm or_false}),
12.21 @@ -488,7 +488,7 @@
12.22 {rew_ord'="tless_true", rls' = Rule.e_rls, calc = [], srls = Rule.e_rls,
12.23 prls = Rule.append_rls "prls_met_simp_poly_minus" Rule.e_rls
12.24 [Rule.Calc ("Poly.is'_polyexp", eval_is_polyexp ""),
12.25 - Rule.Calc ("Tools.matchsub", eval_matchsub ""),
12.26 + Rule.Calc ("Tools.matchsub", Tools.eval_matchsub ""),
12.27 Rule.Thm ("and_true",TermC.num_str @{thm and_true}),
12.28 (*"(?a & True) = ?a"*)
12.29 Rule.Thm ("and_false",TermC.num_str @{thm and_false}),
13.1 --- a/src/Tools/isac/Knowledge/RatEq.thy Mon Dec 31 14:15:19 2018 +0100
13.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy Mon Dec 31 14:49:16 2018 +0100
13.3 @@ -85,9 +85,9 @@
13.4 val RatEq_prls = (*15.10.02:just the following order due to subterm evaluation*)
13.5 Rule.append_rls "RatEq_prls" Rule.e_rls
13.6 [Rule.Calc ("Atools.ident",eval_ident "#ident_"),
13.7 - Rule.Calc ("Tools.matches",eval_matches ""),
13.8 - Rule.Calc ("Tools.lhs" ,eval_lhs ""),
13.9 - Rule.Calc ("Tools.rhs" ,eval_rhs ""),
13.10 + Rule.Calc ("Tools.matches", Tools.eval_matches ""),
13.11 + Rule.Calc ("Tools.lhs" , Tools.eval_lhs ""),
13.12 + Rule.Calc ("Tools.rhs" , Tools.eval_rhs ""),
13.13 Rule.Calc ("RatEq.is'_ratequation'_in",eval_is_ratequation_in ""),
13.14 Rule.Calc ("HOL.eq",eval_equal "#equal_"),
13.15 Rule.Thm ("not_true",TermC.num_str @{thm not_true}),
14.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Mon Dec 31 14:15:19 2018 +0100
14.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Mon Dec 31 14:49:16 2018 +0100
14.3 @@ -205,9 +205,9 @@
14.4 val RootEq_prls =(*15.10.02:just the following order due to subterm evaluation*)
14.5 Rule.append_rls "RootEq_prls" Rule.e_rls
14.6 [Rule.Calc ("Atools.ident",eval_ident "#ident_"),
14.7 - Rule.Calc ("Tools.matches",eval_matches ""),
14.8 - Rule.Calc ("Tools.lhs" ,eval_lhs ""),
14.9 - Rule.Calc ("Tools.rhs" ,eval_rhs ""),
14.10 + Rule.Calc ("Tools.matches", Tools.eval_matches ""),
14.11 + Rule.Calc ("Tools.lhs" , Tools.eval_lhs ""),
14.12 + Rule.Calc ("Tools.rhs" , Tools.eval_rhs ""),
14.13 Rule.Calc ("RootEq.is'_sqrtTerm'_in",eval_is_sqrtTerm_in ""),
14.14 Rule.Calc ("RootEq.is'_rootTerm'_in",eval_is_rootTerm_in ""),
14.15 Rule.Calc ("RootEq.is'_normSqrtTerm'_in",eval_is_normSqrtTerm_in ""),
15.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy Mon Dec 31 14:15:19 2018 +0100
15.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy Mon Dec 31 14:49:16 2018 +0100
15.3 @@ -79,9 +79,9 @@
15.4 val RootRatEq_prls =
15.5 Rule.append_rls "RootRatEq_prls" Rule.e_rls
15.6 [Rule.Calc ("Atools.ident",eval_ident "#ident_"),
15.7 - Rule.Calc ("Tools.matches",eval_matches ""),
15.8 - Rule.Calc ("Tools.lhs" ,eval_lhs ""),
15.9 - Rule.Calc ("Tools.rhs" ,eval_rhs ""),
15.10 + Rule.Calc ("Tools.matches", Tools.eval_matches ""),
15.11 + Rule.Calc ("Tools.lhs" , Tools.eval_lhs ""),
15.12 + Rule.Calc ("Tools.rhs" , Tools.eval_rhs ""),
15.13 Rule.Calc ("RootEq.is'_rootTerm'_in",eval_is_rootTerm_in ""),
15.14 Rule.Calc ("RootRatEq.is'_rootRatAddTerm'_in",
15.15 eval_is_rootRatAddTerm_in ""),
16.1 --- a/src/Tools/isac/Knowledge/Test.thy Mon Dec 31 14:15:19 2018 +0100
16.2 +++ b/src/Tools/isac/Knowledge/Test.thy Mon Dec 31 14:49:16 2018 +0100
16.3 @@ -404,7 +404,7 @@
16.4 Rule.Thm ("or_commute",TermC.num_str @{thm or_commute}),
16.5
16.6 Rule.Calc ("Atools.is'_const",eval_const "#is_const_"),
16.7 - Rule.Calc ("Tools.matches",eval_matches ""),
16.8 + Rule.Calc ("Tools.matches", Tools.eval_matches ""),
16.9
16.10 Rule.Calc ("Groups.plus_class.plus",eval_binop "#add_"),
16.11 Rule.Calc ("Groups.times_class.times",eval_binop "#mult_"),
16.12 @@ -446,7 +446,7 @@
16.13
16.14 Rule.Calc ("Atools.is'_const",eval_const "#is_const_"),
16.15 Rule.Calc ("Test.contains'_root",eval_contains_root "#eval_contains_root"),
16.16 - Rule.Calc ("Tools.matches",eval_matches ""),
16.17 + Rule.Calc ("Tools.matches", Tools.eval_matches ""),
16.18 Rule.Calc ("Test.contains'_root",
16.19 eval_contains_root"#contains_root_"),
16.20
16.21 @@ -593,7 +593,7 @@
16.22 ("isolate_root", (Context.theory_name @{theory}, prep_rls' isolate_root)),
16.23 ("isolate_bdv", (Context.theory_name @{theory}, prep_rls' isolate_bdv)),
16.24 ("matches", (Context.theory_name @{theory}, prep_rls'
16.25 - (Rule.append_rls "matches" testerls [Rule.Calc ("Tools.matches",eval_matches "#matches_")])))]
16.26 + (Rule.append_rls "matches" testerls [Rule.Calc ("Tools.matches", Tools.eval_matches "#matches_")])))]
16.27 \<close>
16.28
16.29 subsection \<open>problems\<close>
17.1 --- a/src/Tools/isac/ProgLang/Atools.thy Mon Dec 31 14:15:19 2018 +0100
17.2 +++ b/src/Tools/isac/ProgLang/Atools.thy Mon Dec 31 14:49:16 2018 +0100
17.3 @@ -507,7 +507,7 @@
17.4 (p as Const ("Atools.boollist2sum", _) $
17.5 (l as Const ("List.list.Cons", _) $ _ $ _)) _ =
17.6 let val isal = TermC.isalist2list l
17.7 - val lhss = map lhs isal
17.8 + val lhss = map Tools.lhs isal
17.9 val sum = list2sum lhss
17.10 in SOME ((Rule.term2str p) ^ " = " ^ (Rule.term2str sum),
17.11 HOLogic.Trueprop $ (TermC.mk_equality (p, sum)))
17.12 @@ -537,7 +537,7 @@
17.13 Rule.Calc ("Atools.ident",eval_ident "#ident_"),
17.14 Rule.Calc ("HOL.eq",eval_equal "#equal_"),(*atom <> atom -> False*)
17.15
17.16 - Rule.Calc ("Tools.Vars",eval_var "#Vars_"),
17.17 + Rule.Calc ("Tools.Vars",Tools.eval_var "#Vars_"),
17.18
17.19 Rule.Thm ("if_True",TermC.num_str @{thm if_True}),
17.20 Rule.Thm ("if_False",TermC.num_str @{thm if_False})
17.21 @@ -598,7 +598,7 @@
17.22 Rule.Calc ("Atools.ident",eval_ident "#ident_"),
17.23 Rule.Calc ("Atools.is'_const",eval_const "#is_const_"),
17.24 Rule.Calc ("Atools.occurs'_in",eval_occurs_in ""),
17.25 - Rule.Calc ("Tools.matches",eval_matches "")
17.26 + Rule.Calc ("Tools.matches", Tools.eval_matches "")
17.27 ];
17.28
17.29 \<close>
17.30 @@ -627,7 +627,7 @@
17.31 Rule.Calc ("Atools.ident",eval_ident "#ident_"),
17.32 Rule.Calc ("Atools.is'_const",eval_const "#is_const_"),
17.33 Rule.Calc ("Atools.occurs'_in",eval_occurs_in ""),
17.34 - Rule.Calc ("Tools.matches",eval_matches "")
17.35 + Rule.Calc ("Tools.matches", Tools.eval_matches "")
17.36 ];
17.37
17.38 (*val atools_erls = ... waere zu testen ...
18.1 --- a/src/Tools/isac/ProgLang/Tools.thy Mon Dec 31 14:15:19 2018 +0100
18.2 +++ b/src/Tools/isac/ProgLang/Tools.thy Mon Dec 31 14:49:16 2018 +0100
18.3 @@ -49,6 +49,25 @@
18.4 *)
18.5
18.6 ML \<open>(*the former Tools.ML*)
18.7 +signature TOOLS =
18.8 + sig
18.9 + val EmptyList: term
18.10 + val UniversalList: term
18.11 + val eval_lhs: 'a -> string -> term -> 'b -> (string * term) option
18.12 + val eval_matches: string -> string -> term -> theory -> (string * term) option
18.13 + val eval_matchsub: string -> string -> term -> theory -> (string * term) option
18.14 + val eval_rhs: 'a -> string -> term -> 'b -> (string * term) option
18.15 + val eval_var: string -> string -> term -> theory -> (string * term) option
18.16 + val lhs: term -> term
18.17 + val list_rls: Rule.rls
18.18 + val matchsub: theory -> term -> term -> bool
18.19 + val or2list: term -> term
18.20 + val rhs: term -> term
18.21 + end
18.22 +
18.23 +structure Tools: TOOLS =
18.24 +struct
18.25 +
18.26 (* auxiliary functions for scripts WN.9.00*)
18.27 (*11.02: for equation solving only*)
18.28 val UniversalList = (Thm.term_of o the o (TermC.parse @{theory})) "UniversalList";
18.29 @@ -219,13 +238,14 @@
18.30 (*for evaluating scripts*)
18.31
18.32 val list_rls = Rule.append_rls "list_rls" list_rls [Rule.Calc ("Tools.rhs", eval_rhs "")];
18.33 +end (*struct*)
18.34 \<close>
18.35 setup \<open>KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))]\<close>
18.36 setup \<open>KEStore_Elems.add_calcs
18.37 - [("matches", ("Tools.matches", eval_matches "#matches_")),
18.38 - ("matchsub", ("Tools.matchsub", eval_matchsub "#matchsub_")),
18.39 - ("Vars", ("Tools.Vars", eval_var "#Vars_")),
18.40 - ("lhs", ("Tools.lhs", eval_lhs "")),
18.41 - ("rhs", ("Tools.rhs", eval_rhs ""))]\<close>
18.42 + [("matches", ("Tools.matches", Tools.eval_matches "#matches_")),
18.43 + ("matchsub", ("Tools.matchsub", Tools.eval_matchsub "#matchsub_")),
18.44 + ("Vars", ("Tools.Vars", Tools.eval_var "#Vars_")),
18.45 + ("lhs", ("Tools.lhs", Tools.eval_lhs "")),
18.46 + ("rhs", ("Tools.rhs", Tools.eval_rhs ""))]\<close>
18.47
18.48 end
19.1 --- a/test/Tools/isac/Test_Isac.thy Mon Dec 31 14:15:19 2018 +0100
19.2 +++ b/test/Tools/isac/Test_Isac.thy Mon Dec 31 14:49:16 2018 +0100
19.3 @@ -166,6 +166,15 @@
19.4 ML_file "Minisubpbl/600-postcond.sml"
19.5 ML \<open>"%%%%%%%%%%%%%%%%% end Minisubpbl.thy %%%%%%%%%%%%%%%%%%%%%%%";\<close>
19.6 ML \<open>"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";\<close>
19.7 +ML \<open>
19.8 +"~~~~~ fun , args:"; val () = ();
19.9 +\<close> ML \<open>
19.10 +Tools.lhs
19.11 +\<close> ML \<open>
19.12 +\<close> ML \<open>
19.13 +\<close> ML \<open>
19.14 +"~~~~~ fun , args:"; val () = ();
19.15 +\<close>
19.16 ML_file "Interpret/mstools.sml"
19.17 ML_file "Interpret/ctree.sml" (*!...!see(25)*)
19.18 ML_file "Interpret/ptyps.sml" (* requires setup from ptyps.thy *)
20.1 --- a/test/Tools/isac/Test_Some.thy Mon Dec 31 14:15:19 2018 +0100
20.2 +++ b/test/Tools/isac/Test_Some.thy Mon Dec 31 14:49:16 2018 +0100
20.3 @@ -27,7 +27,7 @@
20.4 open Rule; string_of_thm;
20.5 (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
20.6 \<close>
20.7 -ML_file "ProgLang/scrtools.sml"
20.8 +ML_file "Interpret/mstools.sml"
20.9
20.10 section \<open>code for copy & paste ===============================================================\<close>
20.11 ML \<open>
20.12 @@ -61,6 +61,7 @@
20.13 ML \<open>
20.14 "~~~~~ fun , args:"; val () = ();
20.15 \<close> ML \<open>
20.16 +lhs
20.17 \<close> ML \<open>
20.18 \<close> ML \<open>
20.19 \<close> ML \<open>