1.1 --- a/src/Tools/isac/Build_Isac.thy Mon Sep 13 18:37:16 2010 +0200
1.2 +++ b/src/Tools/isac/Build_Isac.thy Tue Sep 14 12:12:42 2010 +0200
1.3 @@ -85,8 +85,10 @@
1.4 use_thy "Knowledge/Test"
1.5 *)
1.6 use_thy "Knowledge/Isac"
1.7 -check_guhs_unique := false;
1.8 +ML {* check_guhs_unique := false; *}
1.9 ML {* writeln "**** isac kernel = math-engine + Knowledge complete ******" *}
1.10
1.11 +use "../../../test/Tools/isac/Interpret/calchead.sml"
1.12 +
1.13 end
1.14
2.1 --- a/src/Tools/isac/Interpret/calchead.sml Mon Sep 13 18:37:16 2010 +0200
2.2 +++ b/src/Tools/isac/Interpret/calchead.sml Tue Sep 14 12:12:42 2010 +0200
2.3 @@ -931,9 +931,10 @@
2.4 of a SubProblem ? see ME/ptyps.sml 'type met '.*)
2.5 fun is_copy_named_idstr str =
2.6 case (rev o explode) str of
2.7 - "_"::_::"_"::_ => true
2.8 + (*"_"::_ ::"_"::_ => true*)
2.9 + "'"::"'"::"'"::_ => true
2.10 | _ => false;
2.11 -(*> is_copy_named_idstr "v_i_";
2.12 +(*> is_copy_named_idstr "v_i'''";
2.13 val it = true : bool
2.14 > is_copy_named_idstr "e_";
2.15 val it = false : bool
2.16 @@ -947,7 +948,7 @@
2.17 "_"::"_"::"_"::_ => false
2.18 | _ => true
2.19 else false;
2.20 -(*> is_copy_named_generating_idstr "v_i_";
2.21 +(*> is_copy_named_generating_idstr "v_i'''";
2.22 val it = true : bool
2.23 > is_copy_named_generating_idstr "L___";
2.24 val it = false : bool
3.1 --- a/src/Tools/isac/Interpret/ptyps.sml Mon Sep 13 18:37:16 2010 +0200
3.2 +++ b/src/Tools/isac/Interpret/ptyps.sml Tue Sep 14 12:12:42 2010 +0200
3.3 @@ -356,7 +356,7 @@
3.4 (*.the pattern for an item of a problems model or a methods guard.*)
3.5 type pat = (string * (*field*)
3.6 (term * (*description*)
3.7 - term)) (*id | struct-var*);
3.8 + term)) (*id | arbitrary term*);
3.9 fun pat2str ((field, (dsc, id)):pat) =
3.10 pair2str (field, pair2str (term2str dsc, term2str id));
3.11 fun pats2str pats = (strs2str o (map pat2str)) pats;
3.12 @@ -376,7 +376,7 @@
3.13 nrls : rls, (*canonical simplifier specific for this met *)
3.14 calc : calc list, (*040207: <--- calclist' in fun prep_met *)
3.15 (*branch : TransitiveB set in append_problem at generation ob pblobj
3.16 - FIXXXME.8.03: set branch from met in Apply_Method *)
3.17 + FIXXXME.0308: set branch from met in Apply_Method ? *)
3.18
3.19 (* compare type pbt:*)
3.20 ppc: pat list,
3.21 @@ -385,7 +385,7 @@
3.22 are 'copy-named' with an identifier "*_!_".
3.23 copy-named items are 'generating' if they are NOT "*___"
3.24 see ME/calchead.sml 'fun is_copy_named'.*)
3.25 - pre: term list, (*preconditions in where*)
3.26 + pre: term list, (*preconditions in where*)
3.27 (*script*)
3.28 scr: scr (*prep_met requires either script or string "empty_script"*)
3.29 };
4.1 --- a/src/Tools/isac/Knowledge/Equation.thy Mon Sep 13 18:37:16 2010 +0200
4.2 +++ b/src/Tools/isac/Knowledge/Equation.thy Tue Sep 14 12:12:42 2010 +0200
4.3 @@ -44,7 +44,7 @@
4.4 (["equation"],
4.5 [("#Given" ,["equality e_e","solveFor v_v"]),
4.6 ("#Where" ,["matches (?a = ?b) e_e"]),
4.7 - ("#Find" ,["solutions v_i"])
4.8 + ("#Find" ,["solutions v_i'''"])
4.9 ],
4.10 append_rls "equation_prls" e_rls
4.11 [Calc ("Tools.matches",eval_matches "")],
4.12 @@ -56,7 +56,7 @@
4.13 (["univariate","equation"],
4.14 [("#Given" ,["equality e_e","solveFor v_v"]),
4.15 ("#Where" ,["matches (?a = ?b) e_e"]),
4.16 - ("#Find" ,["solutions v_i"])
4.17 + ("#Find" ,["solutions v_i'''"])
4.18 ],
4.19 univariate_equation_prls,SOME "solve (e_e::bool, v_v)",[]));
4.20
5.1 --- a/src/Tools/isac/Knowledge/LinEq.thy Mon Sep 13 18:37:16 2010 +0200
5.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Tue Sep 14 12:12:42 2010 +0200
5.3 @@ -134,7 +134,7 @@
5.4 "Not( (rhs e_e) is_polyrat_in v_v)",
5.5 "((lhs e_e) has_degree_in v_v)=1",
5.6 "((rhs e_e) has_degree_in v_v)=1"]),
5.7 - ("#Find" ,["solutions v_i"])
5.8 + ("#Find" ,["solutions v_i'''"])
5.9 ],
5.10 LinEq_prls, SOME "solve (e_e::bool, v_v)",
5.11 [["LinEq","solve_lineq_equation"]]));
5.12 @@ -155,7 +155,7 @@
5.13 [("#Given", ["equality e_e", "solveFor v_v"]),
5.14 ("#Where", ["Not ((lhs e_e) is_polyrat_in v_v)",
5.15 "((lhs e_e) has_degree_in v_v) = 1"]),
5.16 - ("#Find", ["solutions v_i"])
5.17 + ("#Find", ["solutions v_i'''"])
5.18 ],
5.19 {rew_ord'="termlessI", rls'=LinEq_erls, srls=e_rls, prls=LinEq_prls,
5.20 calc=[], crls=LinEq_crls, nrls=norm_Poly},
6.1 --- a/src/Tools/isac/Knowledge/LogExp.thy Mon Sep 13 18:37:16 2010 +0200
6.2 +++ b/src/Tools/isac/Knowledge/LogExp.thy Tue Sep 14 12:12:42 2010 +0200
6.3 @@ -33,9 +33,9 @@
6.4 (["logarithmic","univariate","equation"],
6.5 [("#Given",["equality e_e","solveFor v_v"]),
6.6 ("#Where",["matches ((?a log ?v_v) = ?b) e_e"]),
6.7 - ("#Find" ,["solutions v_i"]),
6.8 - ("#With" ,["||(lhs (Subst (v_i_,v_v) e_e) - " ^
6.9 - " (rhs (Subst (v_i_,v_v) e_e) || < eps)"])
6.10 + ("#Find" ,["solutions v_i'''"]),
6.11 + ("#With" ,["||(lhs (Subst (v_i''', v_v) e_e) - " ^
6.12 + " (rhs (Subst (v_i''', v_v) e_e) || < eps)"])
6.13 ],
6.14 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
6.15 [["Equation","solve_log"]]));
6.16 @@ -47,7 +47,7 @@
6.17 (["Equation","solve_log"],
6.18 [("#Given" ,["equality e_e","solveFor v_v"]),
6.19 ("#Where" ,["matches ((?a log ?v_v) = ?b) e_e"]),
6.20 - ("#Find" ,["solutions v_i"])
6.21 + ("#Find" ,["solutions v_i'''"])
6.22 ],
6.23 {rew_ord'="termlessI",rls'=PolyEq_erls,srls=e_rls,prls=PolyEq_prls,
6.24 calc=[],crls=PolyEq_crls, nrls=norm_Rational},
7.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Mon Sep 13 18:37:16 2010 +0200
7.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Tue Sep 14 12:12:42 2010 +0200
7.3 @@ -849,7 +849,7 @@
7.4 ("#Where" ,["~((e_e::bool) is_ratequation_in (v_v::real))",
7.5 "~((lhs e_e) is_rootTerm_in (v_v::real))",
7.6 "~((rhs e_e) is_rootTerm_in (v_v::real))"]),
7.7 - ("#Find" ,["solutions v_i"])
7.8 + ("#Find" ,["solutions v_i'''"])
7.9 ],
7.10 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
7.11 []));
7.12 @@ -862,7 +862,7 @@
7.13 "(lhs e_e) is_poly_in v_v",
7.14 "((lhs e_e) has_degree_in v_v ) = 0"
7.15 ]),
7.16 - ("#Find" ,["solutions v_i"])
7.17 + ("#Find" ,["solutions v_i'''"])
7.18 ],
7.19 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
7.20 [["PolyEq","solve_d0_polyeq_equation"]]));
7.21 @@ -876,7 +876,7 @@
7.22 "(lhs e_e) is_poly_in v_v",
7.23 "((lhs e_e) has_degree_in v_v ) = 1"
7.24 ]),
7.25 - ("#Find" ,["solutions v_i"])
7.26 + ("#Find" ,["solutions v_i'''"])
7.27 ],
7.28 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
7.29 [["PolyEq","solve_d1_polyeq_equation"]]));
7.30 @@ -890,7 +890,7 @@
7.31 ("#Where" ,["matches (?a = 0) e_e",
7.32 "(lhs e_e) is_poly_in v_v ",
7.33 "((lhs e_e) has_degree_in v_v ) = 2"]),
7.34 - ("#Find" ,["solutions v_i"])
7.35 + ("#Find" ,["solutions v_i'''"])
7.36 ],
7.37 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
7.38 [["PolyEq","solve_d2_polyeq_equation"]]));
7.39 @@ -911,7 +911,7 @@
7.40 "Not (matches ( ?b*?v_ + ?v_^^^2 = 0) e_e) &" ^
7.41 "Not (matches ( ?v_ + ?c*?v_^^^2 = 0) e_e) &" ^
7.42 "Not (matches ( ?b*?v_ + ?c*?v_^^^2 = 0) e_e)"]),
7.43 - ("#Find" ,["solutions v_i"])
7.44 + ("#Find" ,["solutions v_i'''"])
7.45 ],
7.46 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
7.47 [["PolyEq","solve_d2_polyeq_sqonly_equation"]]));
7.48 @@ -926,7 +926,7 @@
7.49 "matches (?a*?v_ + ?b*?v_^^^2 = 0) e_e | " ^
7.50 "matches ( ?v_^^^2 = 0) e_e | " ^
7.51 "matches ( ?b*?v_^^^2 = 0) e_e "]),
7.52 - ("#Find" ,["solutions v_i"])
7.53 + ("#Find" ,["solutions v_i'''"])
7.54 ],
7.55 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
7.56 [["PolyEq","solve_d2_polyeq_bdvonly_equation"]]));
7.57 @@ -937,7 +937,7 @@
7.58 [("#Given" ,["equality e_e","solveFor v_v"]),
7.59 ("#Where" ,["matches (?a + 1*?v_^^^2 = 0) e_e | " ^
7.60 "matches (?a + ?v_^^^2 = 0) e_e"]),
7.61 - ("#Find" ,["solutions v_i"])
7.62 + ("#Find" ,["solutions v_i'''"])
7.63 ],
7.64 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
7.65 [["PolyEq","solve_d2_polyeq_pq_equation"]]));
7.66 @@ -948,7 +948,7 @@
7.67 [("#Given" ,["equality e_e","solveFor v_v"]),
7.68 ("#Where" ,["matches (?a + ?v_^^^2 = 0) e_e | " ^
7.69 "matches (?a + ?b*?v_^^^2 = 0) e_e"]),
7.70 - ("#Find" ,["solutions v_i"])
7.71 + ("#Find" ,["solutions v_i'''"])
7.72 ],
7.73 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
7.74 [["PolyEq","solve_d2_polyeq_abc_equation"]]));
7.75 @@ -962,7 +962,7 @@
7.76 ("#Where" ,["matches (?a = 0) e_e",
7.77 "(lhs e_e) is_poly_in v_v ",
7.78 "((lhs e_e) has_degree_in v_v) = 3"]),
7.79 - ("#Find" ,["solutions v_i"])
7.80 + ("#Find" ,["solutions v_i'''"])
7.81 ],
7.82 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
7.83 [["PolyEq","solve_d3_polyeq_equation"]]));
7.84 @@ -975,7 +975,7 @@
7.85 ("#Where" ,["matches (?a = 0) e_e",
7.86 "(lhs e_e) is_poly_in v_v ",
7.87 "((lhs e_e) has_degree_in v_v) = 4"]),
7.88 - ("#Find" ,["solutions v_i"])
7.89 + ("#Find" ,["solutions v_i'''"])
7.90 ],
7.91 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
7.92 [(*["PolyEq","solve_d4_polyeq_equation"]*)]));
7.93 @@ -987,7 +987,7 @@
7.94 [("#Given" ,["equality e_e","solveFor v_v"]),
7.95 ("#Where" ,["(Not((matches (?a = 0 ) e_e ))) |" ^
7.96 "(Not(((lhs e_e) is_poly_in v_v)))"]),
7.97 - ("#Find" ,["solutions v_i"])
7.98 + ("#Find" ,["solutions v_i'''"])
7.99 ],
7.100 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
7.101 [["PolyEq","normalize_poly"]]));
7.102 @@ -998,7 +998,7 @@
7.103 [("#Given" ,["equality e_e","solveFor v_v"]),
7.104 ("#Where" ,["matches (?a = 0) e_e",
7.105 "(lhs e_e) is_expanded_in v_v "]),
7.106 - ("#Find" ,["solutions v_i"])
7.107 + ("#Find" ,["solutions v_i'''"])
7.108 ],
7.109 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
7.110 []));
7.111 @@ -1009,7 +1009,7 @@
7.112 (["degree_2","expanded","univariate","equation"],
7.113 [("#Given" ,["equality e_e","solveFor v_v"]),
7.114 ("#Where" ,["((lhs e_e) has_degree_in v_v) = 2"]),
7.115 - ("#Find" ,["solutions v_i"])
7.116 + ("#Find" ,["solutions v_i'''"])
7.117 ],
7.118 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
7.119 [["PolyEq","complete_square"]]));
7.120 @@ -1043,7 +1043,7 @@
7.121 [("#Given" ,["equality e_e","solveFor v_v"]),
7.122 ("#Where" ,["(Not((matches (?a = 0 ) e_e ))) |" ^
7.123 "(Not(((lhs e_e) is_poly_in v_v)))"]),
7.124 - ("#Find" ,["solutions v_i"])
7.125 + ("#Find" ,["solutions v_i'''"])
7.126 ],
7.127 {rew_ord'="termlessI",
7.128 rls'=PolyEq_erls,
7.129 @@ -1070,7 +1070,7 @@
7.130 [("#Given" ,["equality e_e","solveFor v_v"]),
7.131 ("#Where" ,["(lhs e_e) is_poly_in v_v ",
7.132 "((lhs e_e) has_degree_in v_v) = 0"]),
7.133 - ("#Find" ,["solutions v_i"])
7.134 + ("#Find" ,["solutions v_i'''"])
7.135 ],
7.136 {rew_ord'="termlessI",
7.137 rls'=PolyEq_erls,
7.138 @@ -1091,7 +1091,7 @@
7.139 [("#Given" ,["equality e_e","solveFor v_v"]),
7.140 ("#Where" ,["(lhs e_e) is_poly_in v_v ",
7.141 "((lhs e_e) has_degree_in v_v) = 1"]),
7.142 - ("#Find" ,["solutions v_i"])
7.143 + ("#Find" ,["solutions v_i'''"])
7.144 ],
7.145 {rew_ord'="termlessI", rls'=PolyEq_erls, srls=e_rls, prls=PolyEq_prls,
7.146 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
7.147 @@ -1112,7 +1112,7 @@
7.148 [("#Given" ,["equality e_e","solveFor v_v"]),
7.149 ("#Where" ,["(lhs e_e) is_poly_in v_v ",
7.150 "((lhs e_e) has_degree_in v_v) = 2"]),
7.151 - ("#Find" ,["solutions v_i"])
7.152 + ("#Find" ,["solutions v_i'''"])
7.153 ],
7.154 {rew_ord'="termlessI",
7.155 rls'=PolyEq_erls,
7.156 @@ -1139,7 +1139,7 @@
7.157 [("#Given" ,["equality e_e","solveFor v_v"]),
7.158 ("#Where" ,["(lhs e_e) is_poly_in v_v ",
7.159 "((lhs e_e) has_degree_in v_v) = 2"]),
7.160 - ("#Find" ,["solutions v_i"])
7.161 + ("#Find" ,["solutions v_i'''"])
7.162 ],
7.163 {rew_ord'="termlessI",
7.164 rls'=PolyEq_erls,
7.165 @@ -1166,7 +1166,7 @@
7.166 [("#Given" ,["equality e_e","solveFor v_v"]),
7.167 ("#Where" ,["(lhs e_e) is_poly_in v_v ",
7.168 "((lhs e_e) has_degree_in v_v) = 2"]),
7.169 - ("#Find" ,["solutions v_i"])
7.170 + ("#Find" ,["solutions v_i'''"])
7.171 ],
7.172 {rew_ord'="termlessI",
7.173 rls'=PolyEq_erls,
7.174 @@ -1190,7 +1190,7 @@
7.175 [("#Given" ,["equality e_e","solveFor v_v"]),
7.176 ("#Where" ,["(lhs e_e) is_poly_in v_v ",
7.177 "((lhs e_e) has_degree_in v_v) = 2"]),
7.178 - ("#Find" ,["solutions v_i"])
7.179 + ("#Find" ,["solutions v_i'''"])
7.180 ],
7.181 {rew_ord'="termlessI",
7.182 rls'=PolyEq_erls,
7.183 @@ -1214,7 +1214,7 @@
7.184 [("#Given" ,["equality e_e","solveFor v_v"]),
7.185 ("#Where" ,["(lhs e_e) is_poly_in v_v ",
7.186 "((lhs e_e) has_degree_in v_v) = 2"]),
7.187 - ("#Find" ,["solutions v_i"])
7.188 + ("#Find" ,["solutions v_i'''"])
7.189 ],
7.190 {rew_ord'="termlessI",
7.191 rls'=PolyEq_erls,
7.192 @@ -1238,7 +1238,7 @@
7.193 [("#Given" ,["equality e_e","solveFor v_v"]),
7.194 ("#Where" ,["(lhs e_e) is_poly_in v_v ",
7.195 "((lhs e_e) has_degree_in v_v) = 3"]),
7.196 - ("#Find" ,["solutions v_i"])
7.197 + ("#Find" ,["solutions v_i'''"])
7.198 ],
7.199 {rew_ord'="termlessI",
7.200 rls'=PolyEq_erls,
7.201 @@ -1271,7 +1271,7 @@
7.202 [("#Given" ,["equality e_e","solveFor v_v"]),
7.203 ("#Where" ,["matches (?a = 0) e_e",
7.204 "((lhs e_e) has_degree_in v_v) = 2"]),
7.205 - ("#Find" ,["solutions v_i"])
7.206 + ("#Find" ,["solutions v_i'''"])
7.207 ],
7.208 {rew_ord'="termlessI",rls'=PolyEq_erls,srls=e_rls,prls=PolyEq_prls,
7.209 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
8.1 --- a/src/Tools/isac/Knowledge/RatEq.thy Mon Sep 13 18:37:16 2010 +0200
8.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy Tue Sep 14 12:12:42 2010 +0200
8.3 @@ -175,7 +175,7 @@
8.4 (["rational","univariate","equation"],
8.5 [("#Given" ,["equality e_e","solveFor v_v"]),
8.6 ("#Where" ,["(e_e::bool) is_ratequation_in (v_v::real)"]),
8.7 - ("#Find" ,["solutions v_i"])
8.8 + ("#Find" ,["solutions v_i'''"])
8.9 ],
8.10
8.11 RatEq_prls, SOME "solve (e_e::bool, v_v)",
8.12 @@ -199,7 +199,7 @@
8.13 (["RatEq","solve_rat_equation"],
8.14 [("#Given" ,["equality e_e","solveFor v_v"]),
8.15 ("#Where" ,["(e_e::bool) is_ratequation_in (v_v::real)"]),
8.16 - ("#Find" ,["solutions v_i"])
8.17 + ("#Find" ,["solutions v_i'''"])
8.18 ],
8.19 {rew_ord'="termlessI",
8.20 rls'=rateq_erls,
9.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Mon Sep 13 18:37:16 2010 +0200
9.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Tue Sep 14 12:12:42 2010 +0200
9.3 @@ -482,7 +482,7 @@
9.4 [("#Given" ,["equality e_e","solveFor v_v"]),
9.5 ("#Where" ,["(lhs e_e) is_rootTerm_in (v_v::real) | " ^
9.6 "(rhs e_e) is_rootTerm_in (v_v::real)"]),
9.7 - ("#Find" ,["solutions v_i"])
9.8 + ("#Find" ,["solutions v_i'''"])
9.9 ],
9.10 RootEq_prls, SOME "solve (e_e::bool, v_v)",
9.11 []));
9.12 @@ -495,7 +495,7 @@
9.13 " ((lhs e_e) is_normSqrtTerm_in (v_v::real)) ) |" ^
9.14 "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
9.15 " ((rhs e_e) is_normSqrtTerm_in (v_v::real)) )"]),
9.16 - ("#Find" ,["solutions v_i"])
9.17 + ("#Find" ,["solutions v_i'''"])
9.18 ],
9.19 RootEq_prls, SOME "solve (e_e::bool, v_v)",
9.20 [["RootEq","solve_sq_root_equation"]]));
9.21 @@ -508,7 +508,7 @@
9.22 " Not((lhs e_e) is_normSqrtTerm_in (v_v::real))) | " ^
9.23 "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
9.24 " Not((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]),
9.25 - ("#Find" ,["solutions v_i"])
9.26 + ("#Find" ,["solutions v_i'''"])
9.27 ],
9.28 RootEq_prls, SOME "solve (e_e::bool, v_v)",
9.29 [["RootEq","norm_sq_root_equation"]]));
9.30 @@ -532,7 +532,7 @@
9.31 " Not((lhs e_e) is_normSqrtTerm_in (v_v::real))) | " ^
9.32 "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
9.33 " Not((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]),
9.34 - ("#Find" ,["solutions v_i"])
9.35 + ("#Find" ,["solutions v_i'''"])
9.36 ],
9.37 {rew_ord'="termlessI", rls'=RootEq_erls, srls=e_rls, prls=RootEq_prls,
9.38 calc=[], crls=RootEq_crls, nrls=norm_Poly},
9.39 @@ -558,7 +558,7 @@
9.40 " ((lhs e_e) is_normSqrtTerm_in (v_v::real))) |" ^
9.41 "(((rhs e_e) is_sqrtTerm_in (v_v::real)) & " ^
9.42 " ((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]),
9.43 - ("#Find" ,["solutions v_i"])
9.44 + ("#Find" ,["solutions v_i'''"])
9.45 ],
9.46 {rew_ord'="termlessI", rls'=RootEq_erls, srls = rooteq_srls,
9.47 prls = RootEq_prls, calc = [], crls=RootEq_crls, nrls=norm_Poly},
9.48 @@ -586,7 +586,7 @@
9.49 (["RootEq","solve_right_sq_root_equation"],
9.50 [("#Given" ,["equality e_e","solveFor v_v"]),
9.51 ("#Where" ,["(rhs e_e) is_sqrtTerm_in v_v"]),
9.52 - ("#Find" ,["solutions v_i"])
9.53 + ("#Find" ,["solutions v_i'''"])
9.54 ],
9.55 {rew_ord' = "termlessI", rls' = RootEq_erls, srls = e_rls,
9.56 prls = RootEq_prls, calc = [], crls = RootEq_crls, nrls = norm_Poly},
9.57 @@ -611,7 +611,7 @@
9.58 (["RootEq","solve_left_sq_root_equation"],
9.59 [("#Given" ,["equality e_e","solveFor v_v"]),
9.60 ("#Where" ,["(lhs e_e) is_sqrtTerm_in v_v"]),
9.61 - ("#Find" ,["solutions v_i"])
9.62 + ("#Find" ,["solutions v_i'''"])
9.63 ],
9.64 {rew_ord'="termlessI",
9.65 rls'=RootEq_erls,
10.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy Mon Sep 13 18:37:16 2010 +0200
10.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy Tue Sep 14 12:12:42 2010 +0200
10.3 @@ -144,7 +144,7 @@
10.4 [("#Given" ,["equality e_e","solveFor v_v"]),
10.5 ("#Where" ,["( (lhs e_e) is_rootRatAddTerm_in (v_v::real) )| " ^
10.6 "( (rhs e_e) is_rootRatAddTerm_in (v_v::real) )"]),
10.7 - ("#Find" ,["solutions v_i"])
10.8 + ("#Find" ,["solutions v_i'''"])
10.9 ],
10.10 RootRatEq_prls, SOME "solve (e_e::bool, v_v)",
10.11 [["RootRatEq","elim_rootrat_equation"]]));
10.12 @@ -164,7 +164,7 @@
10.13 [("#Given" ,["equality e_e","solveFor v_v"]),
10.14 ("#Where" ,["( (lhs e_e) is_rootRatAddTerm_in (v_v::real) ) | " ^
10.15 "( (rhs e_e) is_rootRatAddTerm_in (v_v::real) )"]),
10.16 - ("#Find" ,["solutions v_i"])
10.17 + ("#Find" ,["solutions v_i'''"])
10.18 ],
10.19 {rew_ord'="termlessI",
10.20 rls'=RooRatEq_erls,
11.1 --- a/src/Tools/isac/Knowledge/Test.thy Mon Sep 13 18:37:16 2010 +0200
11.2 +++ b/src/Tools/isac/Knowledge/Test.thy Tue Sep 14 12:12:42 2010 +0200
11.3 @@ -522,7 +522,7 @@
11.4 (["equation","test"],
11.5 [("#Given" ,["equality e_e","solveFor v_v"]),
11.6 ("#Where" ,["matches (?a = ?b) e_e"]),
11.7 - ("#Find" ,["solutions v_i"])
11.8 + ("#Find" ,["solutions v_i'''"])
11.9 ],
11.10 assoc_rls "matches",
11.11 SOME "solve (e_e::bool, v_v)", []));
11.12 @@ -532,7 +532,7 @@
11.13 (["univariate","equation","test"],
11.14 [("#Given" ,["equality e_e","solveFor v_v"]),
11.15 ("#Where" ,["matches (?a = ?b) e_e"]),
11.16 - ("#Find" ,["solutions v_i"])
11.17 + ("#Find" ,["solutions v_i'''"])
11.18 ],
11.19 assoc_rls "matches",
11.20 SOME "solve (e_e::bool, v_v)", []));
11.21 @@ -543,7 +543,7 @@
11.22 [("#Given" ,["equality e_e","solveFor v_v"]),
11.23 ("#Where" ,["(matches ( v_v = 0) e_e) | (matches ( ?b*v_v = 0) e_e) |" ^
11.24 "(matches (?a+v_v = 0) e_e) | (matches (?a+?b*v_v = 0) e_e) "]),
11.25 - ("#Find" ,["solutions v_i"])
11.26 + ("#Find" ,["solutions v_i'''"])
11.27 ],
11.28 assoc_rls "matches",
11.29 SOME "solve (e_e::bool, v_v)", [["Test","solve_linear"]]));
11.30 @@ -595,7 +595,7 @@
11.31 (["Test","solve_linear"]:metID,
11.32 [("#Given" ,["equality e_e","solveFor v_v"]),
11.33 ("#Where" ,["matches (?a = ?b) e_e"]),
11.34 - ("#Find" ,["solutions v_i"])
11.35 + ("#Find" ,["solutions v_i'''"])
11.36 ],
11.37 {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = e_rls,
11.38 prls = assoc_rls "matches", calc = [], crls = tval_rls,
11.39 @@ -783,7 +783,7 @@
11.40 "(matches ( ?b*v_v ^^^2 = 0) e_e) |" ^
11.41 "(matches (?a + v_v ^^^2 = 0) e_e) |" ^
11.42 "(matches ( v_v ^^^2 = 0) e_e)"]),
11.43 - ("#Find" ,["solutions v_i"])
11.44 + ("#Find" ,["solutions v_i'''"])
11.45 ],
11.46 assoc_rls "matches",
11.47 SOME "solve (e_e::bool, v_v)", [["Test","solve_plain_square"]]));
11.48 @@ -817,7 +817,7 @@
11.49 (["polynomial","univariate","equation","test"],
11.50 [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
11.51 ("#Where" ,["False"]),
11.52 - ("#Find" ,["solutions v_i"])
11.53 + ("#Find" ,["solutions v_i'''"])
11.54 ],
11.55 e_rls, SOME "solve (e_e::bool, v_v)", []));
11.56
11.57 @@ -825,7 +825,7 @@
11.58 (prep_pbt thy "pbl_test_uni_poly_deg2" [] e_pblID
11.59 (["degree_two","polynomial","univariate","equation","test"],
11.60 [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
11.61 - ("#Find" ,["solutions v_i"])
11.62 + ("#Find" ,["solutions v_i'''"])
11.63 ],
11.64 e_rls, SOME "solve (v_v ^^^2 + p_p * v_v + q__q = 0, v_v)", []));
11.65
11.66 @@ -833,7 +833,7 @@
11.67 (prep_pbt thy "pbl_test_uni_poly_deg2_pq" [] e_pblID
11.68 (["pq_formula","degree_two","polynomial","univariate","equation","test"],
11.69 [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
11.70 - ("#Find" ,["solutions v_i"])
11.71 + ("#Find" ,["solutions v_i'''"])
11.72 ],
11.73 e_rls, SOME "solve (v_v ^^^2 + p_p * v_v + q__q = 0, v_v)", []));
11.74
11.75 @@ -841,7 +841,7 @@
11.76 (prep_pbt thy "pbl_test_uni_poly_deg2_abc" [] e_pblID
11.77 (["abc_formula","degree_two","polynomial","univariate","equation","test"],
11.78 [("#Given" ,["equality (a_a * x ^^^2 + b_b * x + c_c = 0)","solveFor v_v"]),
11.79 - ("#Find" ,["solutions v_i"])
11.80 + ("#Find" ,["solutions v_i'''"])
11.81 ],
11.82 e_rls, SOME "solve (a_a * x ^^^2 + b_b * x + c_c = 0, v_v)", []));
11.83
11.84 @@ -852,7 +852,7 @@
11.85 (["squareroot","univariate","equation","test"],
11.86 [("#Given" ,["equality e_e","solveFor v_v"]),
11.87 ("#Where" ,["contains_root (e_e::bool)"]),
11.88 - ("#Find" ,["solutions v_i"])
11.89 + ("#Find" ,["solutions v_i'''"])
11.90 ],
11.91 append_rls "contains_root" e_rls [Calc ("Test.contains'_root",
11.92 eval_contains_root "#contains_root_")],
11.93 @@ -863,7 +863,7 @@
11.94 (["normalize","univariate","equation","test"],
11.95 [("#Given" ,["equality e_e","solveFor v_v"]),
11.96 ("#Where" ,[]),
11.97 - ("#Find" ,["solutions v_i"])
11.98 + ("#Find" ,["solutions v_i'''"])
11.99 ],
11.100 e_rls, SOME "solve (e_e::bool, v_v)", [["Test","norm_univar_equation"]]));
11.101
11.102 @@ -872,7 +872,7 @@
11.103 (["sqroot-test","univariate","equation","test"],
11.104 [("#Given" ,["equality e_e","solveFor v_v"]),
11.105 (*("#Where" ,["contains_root (e_e::bool)"]),*)
11.106 - ("#Find" ,["solutions v_i"])
11.107 + ("#Find" ,["solutions v_i'''"])
11.108 ],
11.109 e_rls, SOME "solve (e_e::bool, v_v)", []));
11.110
11.111 @@ -889,7 +889,7 @@
11.112 (["Test","sqrt-equ-test"]:metID,
11.113 [("#Given" ,["equality e_e","solveFor v_v"]),
11.114 ("#Where" ,["contains_root (e_e::bool)"]),
11.115 - ("#Find" ,["solutions v_i"])
11.116 + ("#Find" ,["solutions v_i'''"])
11.117 ],
11.118 {rew_ord'="e_rew_ord",rls'=tval_rls,
11.119 srls =append_rls "srls_contains_root" e_rls
11.120 @@ -923,7 +923,7 @@
11.121 (*root-equation ... for test-*.sml until 8.01*)
11.122 (["Test","squ-equ-test2"]:metID,
11.123 [("#Given" ,["equality e_e","solveFor v_v"]),
11.124 - ("#Find" ,["solutions v_i"])
11.125 + ("#Find" ,["solutions v_i'''"])
11.126 ],
11.127 {rew_ord'="e_rew_ord",rls'=tval_rls,
11.128 srls = append_rls "srls_contains_root" e_rls
11.129 @@ -957,7 +957,7 @@
11.130 (*tests subproblem fixed linear*)
11.131 (["Test","squ-equ-test-subpbl1"]:metID,
11.132 [("#Given" ,["equality e_e","solveFor v_v"]),
11.133 - ("#Find" ,["solutions v_i"])
11.134 + ("#Find" ,["solutions v_i'''"])
11.135 ],
11.136 {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[],
11.137 crls=tval_rls, nrls=Test_simplify},
11.138 @@ -978,7 +978,7 @@
11.139 (*tests subproblem fixed degree 2*)
11.140 (["Test","squ-equ-test-subpbl2"]:metID,
11.141 [("#Given" ,["equality e_e","solveFor v_v"]),
11.142 - ("#Find" ,["solutions v_i"])
11.143 + ("#Find" ,["solutions v_i'''"])
11.144 ],
11.145 {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[],
11.146 crls=tval_rls, nrls=e_rls(*,
11.147 @@ -998,7 +998,7 @@
11.148 (*root-equation: see foils..., but notTerminating*)
11.149 (["Test","square_equation...notTerminating"]:metID,
11.150 [("#Given" ,["equality e_e","solveFor v_v"]),
11.151 - ("#Find" ,["solutions v_i"])
11.152 + ("#Find" ,["solutions v_i'''"])
11.153 ],
11.154 {rew_ord'="e_rew_ord",rls'=tval_rls,
11.155 srls = append_rls "srls_contains_root" e_rls
11.156 @@ -1031,7 +1031,7 @@
11.157 (*root-equation1:*)
11.158 (["Test","square_equation1"]:metID,
11.159 [("#Given" ,["equality e_e","solveFor v_v"]),
11.160 - ("#Find" ,["solutions v_i"])
11.161 + ("#Find" ,["solutions v_i'''"])
11.162 ],
11.163 {rew_ord'="e_rew_ord",rls'=tval_rls,
11.164 srls = append_rls "srls_contains_root" e_rls
11.165 @@ -1063,7 +1063,7 @@
11.166 (*root-equation2*)
11.167 (["Test","square_equation2"]:metID,
11.168 [("#Given" ,["equality e_e","solveFor v_v"]),
11.169 - ("#Find" ,["solutions v_i"])
11.170 + ("#Find" ,["solutions v_i'''"])
11.171 ],
11.172 {rew_ord'="e_rew_ord",rls'=tval_rls,
11.173 srls = append_rls "srls_contains_root" e_rls
11.174 @@ -1096,7 +1096,7 @@
11.175 (*root-equation*)
11.176 (["Test","square_equation"]:metID,
11.177 [("#Given" ,["equality e_e","solveFor v_v"]),
11.178 - ("#Find" ,["solutions v_i"])
11.179 + ("#Find" ,["solutions v_i'''"])
11.180 ],
11.181 {rew_ord'="e_rew_ord",rls'=tval_rls,
11.182 srls = append_rls "srls_contains_root" e_rls
11.183 @@ -1133,7 +1133,7 @@
11.184 "(matches ( ?b*v_v ^^^2 = 0) e_e) |" ^
11.185 "(matches (?a + v_v ^^^2 = 0) e_e) |" ^
11.186 "(matches ( v_v ^^^2 = 0) e_e)"]),
11.187 - ("#Find" ,["solutions v_i"])
11.188 + ("#Find" ,["solutions v_i'''"])
11.189 ],
11.190 {rew_ord'="e_rew_ord",rls'=tval_rls,calc=[],srls=e_rls,
11.191 prls = assoc_rls "matches",
11.192 @@ -1155,7 +1155,7 @@
11.193 (["Test","norm_univar_equation"]:metID,
11.194 [("#Given",["equality e_e","solveFor v_v"]),
11.195 ("#Where" ,[]),
11.196 - ("#Find" ,["solutions v_i"])
11.197 + ("#Find" ,["solutions v_i'''"])
11.198 ],
11.199 {rew_ord'="e_rew_ord",rls'=tval_rls,srls = e_rls,prls=e_rls,
11.200 calc=[],
12.1 --- a/test/Tools/isac/Interpret/calchead.sml Mon Sep 13 18:37:16 2010 +0200
12.2 +++ b/test/Tools/isac/Interpret/calchead.sml Tue Sep 14 12:12:42 2010 +0200
12.3 @@ -10,6 +10,7 @@
12.4 "-----------------------------------------------------------------";
12.5 "table of contents -----------------------------------------------";
12.6 "-----------------------------------------------------------------";
12.7 +"--------- regression test fun is_copy_named ---------------------";
12.8 "--------- get_interval after replace} other 2 -------------------";
12.9 "--------- maximum example with 'specify' ------------------------";
12.10 "--------- maximum example with 'specify', fmz <> [] -------------";
12.11 @@ -20,6 +21,24 @@
12.12 "-----------------------------------------------------------------";
12.13
12.14
12.15 +"--------- regression test fun is_copy_named ---------------------";
12.16 +"--------- regression test fun is_copy_named ---------------------";
12.17 +"--------- regression test fun is_copy_named ---------------------";
12.18 +val trm = (1, (2, @{term "v_i'''"}));
12.19 +if is_copy_named trm then () else raise error "regr. is_copy_named";
12.20 +val trm = (1, (2, @{term "e_e"}));
12.21 +if is_copy_named trm then raise error "regr. is_copy_named" else ();
12.22 +val trm = (1, (2, @{term "L'''"}));
12.23 +if is_copy_named trm then () else raise error "regr. is_copy_named";
12.24 +
12.25 +(* out-comment 'structure CalcHead'...
12.26 +val trm = (1, (2, @{term "v_i'''"}));
12.27 +if is_copy_named_generating trm then () else raise error "regr. is_copy_named";
12.28 +val trm = (1, (2, @{term "L'''"}));
12.29 +if is_copy_named_generating trm then raise error "regr. is_copy_named" else ();
12.30 +*)
12.31 +
12.32 +(*==========================================================================
12.33 "--------- get_interval after replace} other 2 -------------------";
12.34 "--------- get_interval after replace} other 2 -------------------";
12.35 "--------- get_interval after replace} other 2 -------------------";
12.36 @@ -411,3 +430,5 @@
12.37 (* type of Find: [Free ("x_i", "bool List.list")]*)
12.38 => ()
12.39 | _ => raise error "calchead.sml match_ags [univariate,equation,test]--";
12.40 +
12.41 +==========================================================================*)
13.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
13.2 +++ b/test/Tools/isac/ProgLang/term.sml Tue Sep 14 12:12:42 2010 +0200
13.3 @@ -0,0 +1,168 @@
13.4 +(* tests on Scripts/term_G.sml
13.5 + author: Walther Neuper
13.6 + 051006,
13.7 + (c) due to copyright terms
13.8 +
13.9 +use"../smltest/Scripts/term_G.sml";
13.10 +use"term_G.sml";
13.11 +*)
13.12 +
13.13 +"-----------------------------------------------------------------";
13.14 +"table of contents -----------------------------------------------";
13.15 +"-----------------------------------------------------------------";
13.16 +"----------- inst_bdv --------------------------------------------";
13.17 +"----------- subst_atomic_all ------------------------------------";
13.18 +"----------- Pattern.match ---------------------------------------";
13.19 +"----------- fun matches -----------------------------------------";
13.20 +"------------parse------------------------------------------------";
13.21 +"----------- uminus_to_string ------------------------------------";
13.22 +"-----------------------------------------------------------------";
13.23 +"-----------------------------------------------------------------";
13.24 +
13.25 +
13.26 +"----------- inst_bdv --------------------------------------------";
13.27 +"----------- inst_bdv --------------------------------------------";
13.28 +"----------- inst_bdv --------------------------------------------";
13.29 +if string_of_thm (num_str @{thm d1_isolate_add2}) =
13.30 + "\"~ ?bdv occurs_in ?a ==> (?a + ?bdv = 0) = (?bdv = -1 * ?a)\"" then ()
13.31 +else raise error "term_G.sml d1_isolate_add2";
13.32 +val subst = [(str2term "bdv", str2term "x")];
13.33 +val t = (norm o #prop o rep_thm) (num_str @{thm d1_isolate_add2});
13.34 +val t' = inst_bdv subst t;
13.35 +if term2str t' = "~ x occurs_in ?a ==> (?a + x = 0) = (x = -1 * ?a)" then ()
13.36 +else raise error "term_G.sml inst_bdv 1";
13.37 +
13.38 +if string_of_thm (num_str @{thm separate_bdvs_add}) =
13.39 + "\"[] from_ [?bdv_1.0, ?bdv_2.0, ?bdv_3.0, ?bdv_4.0] occur_exactly_in ?a\n\
13.40 + \ ==> (?a + ?b = ?c) = (?b = ?c + -1 * ?a)\"" then ()
13.41 +else raise error "term_G.sml separate_bdvs_add";
13.42 +val subst = [(str2term"bdv_1",str2term"c"),
13.43 + (str2term"bdv_2",str2term"c_2"),
13.44 + (str2term"bdv_3",str2term"c_3"),
13.45 + (str2term"bdv_4",str2term"c_4")];
13.46 +val t = (norm o #prop o rep_thm) (num_str @{thm separate_bdvs_add});
13.47 +val t' = inst_bdv subst t;
13.48 +if term2str t' = "[] from_ [c, c_2, c_3, c_4] occur_exactly_in ?a\n\
13.49 + \==> (?a + ?b = ?c) = (?b = ?c + -1 * ?a)" then ()
13.50 +else raise error "term_G.sml inst_bdv 2";
13.51 +
13.52 +
13.53 +"----------- subst_atomic_all ------------------------------------";
13.54 +"----------- subst_atomic_all ------------------------------------";
13.55 +"----------- subst_atomic_all ------------------------------------";
13.56 +val t = str2term"(tl vs_) from_ vs_ occur_exactly_in (nth_ 1(es_::bool list))";
13.57 +val env = [(str2term"vs_::real list",str2term"[c, c_2]"),
13.58 + (str2term"es_::bool list",str2term"[c_2=0, c+c_2=1]")];
13.59 +val (all_Free_subst, t') = subst_atomic_all env t;
13.60 +if all_Free_subst andalso
13.61 + term2str t' = "tl [c, c_2] from_ [c, c_2] occur_exactly_in nth_ 1 [c_2 = 0, c + c_2 = 1]" then ()
13.62 +else raise error "term_G.sml subst_atomic_all should be 'true'";
13.63 +
13.64 +
13.65 +val (all_Free_subst, t') = subst_atomic_all (tl env) t;
13.66 +if not all_Free_subst andalso
13.67 + term2str t' = "tl vs_ from_ vs_ occur_exactly_in nth_ 1 [c_2 = 0, c + c_2 = 1]" then ()
13.68 +else raise error "term_G.sml subst_atomic_all should be 'false'";
13.69 +
13.70 +
13.71 +"----------- Pattern.match ---------------------------------------";
13.72 +"----------- Pattern.match ---------------------------------------";
13.73 +"----------- Pattern.match ---------------------------------------";
13.74 +val t = (term_of o the o (parse thy)) "3 * x^^^2 = 1";
13.75 +val pat = (free2var o term_of o the o (parse thy)) "a * b^^^2 = c";
13.76 +(* !^^^^^^^^!... necessary for Pattern.match*)
13.77 +val insts = Pattern.match (Sign.tsig_of (sign_of thy)) (pat, t);
13.78 +(*val insts =
13.79 + ([],
13.80 + [(("c",0),Free ("1","RealDef.real")),(("b",0),Free ("x","RealDef.real")),
13.81 + (("a",0),Free ("3","RealDef.real"))])
13.82 + : (indexname * typ) list * (indexname * term) list*)
13.83 +
13.84 +"----- throws exn MATCH...";
13.85 +val t = str2term "x";
13.86 +(Pattern.match (Sign.tsig_of (sign_of thy)) (pat, t))
13.87 +handle MATCH => ([(* (Term.indexname * Term.typ) *)],
13.88 + [(* (Term.indexname * Term.term) *)]);
13.89 +Pattern.MATCH;
13.90 +
13.91 +(*ML {**)
13.92 +val thy = @{theory "Complex_Main"};
13.93 +val PARSE = Syntax.read_term_global thy;
13.94 +val (pa, tm) = (PARSE "a + b::real", PARSE "x + 2*z::real");
13.95 +"-------";
13.96 +val (tye, tme) =
13.97 + (Vartab.empty : Type.tyenv, Vartab.empty : Envir.tenv);
13.98 +"-------";
13.99 +val (tye, tme) = Pattern.match thy (Logic.varify pa, tm) (Vartab.empty,
13.100 + Vartab.empty);
13.101 +"-------";
13.102 +val (tyenv, tenv) = Pattern.match thy (Logic.varify pa, tm)
13.103 + (Vartab.empty, Vartab.empty);
13.104 +Vartab.dest tenv;
13.105 +match thy tm (Logic.varify pa);
13.106 +
13.107 +(**}*)
13.108 +
13.109 +"----------- fun matches -----------------------------------------";
13.110 +"----------- fun matches -----------------------------------------";
13.111 +"----------- fun matches -----------------------------------------";
13.112 +(*smltest/IsacKnowledge/polyeq.sml:
13.113 + Where=[Correct "matches (?a = 0) (-8 - 2 * x + x ^^^ 2 = 0)"*)
13.114 +(*smltest/ME/ptyps.sml:
13.115 + |\nmatches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"],*)
13.116 +(*ML {**)
13.117 +val thy = @{theory "Complex_Main"};
13.118 +"----- test 1";
13.119 +val pa = Logic.varify @{term "a = (0::real)"};
13.120 +"----- test 1 true";
13.121 +val tm = @{term "-8 - 2 * x + x ^ 2 = (0::real)"};
13.122 +if matches thy tm pa then ()
13.123 + else error "term_G.sml diff.behav. in matches true";
13.124 +"----- test 2 false";
13.125 +val tm = @{term "-8 - 2 * x + x ^ 2 = (3::real)"};
13.126 +if matches thy tm pa then error "term_G.sml diff.behav. in matches false"
13.127 + else ();
13.128 +(**}*)
13.129 +
13.130 +"------------parse------------------------------------------------";
13.131 +"------------parse------------------------------------------------";
13.132 +"------------parse------------------------------------------------";
13.133 +(*ML {**)
13.134 +Toplevel.debug := true;
13.135 +(* literal types:
13.136 +PolyML.addPrettyPrinter
13.137 + (fn _ => fn _ => ml_pretty o Pretty.to_ML o raw_pp_typ);
13.138 +*)(* pretty types:
13.139 +PolyML.addPrettyPrinter
13.140 + (fn _ => fn _ => ml_pretty o Pretty.to_ML o Proof_Display.pp_typ Pure.thy);
13.141 +print_depth 99;
13.142 +*)
13.143 +val thy = @{theory "Complex_Main"};
13.144 +val str = "x + z";
13.145 +parse thy str;
13.146 +"---------------";
13.147 +val str = "x + 2*z";
13.148 +val t = (Syntax.read_term_global thy str);
13.149 +val t = numbers_to_string (Syntax.read_term_global thy str);
13.150 +val t = (typ_a2real o numbers_to_string) (Syntax.read_term_global thy str);
13.151 +cterm_of thy t;
13.152 +val t = (the (parse thy str)) handle _ => error "term_G.sml parsing 'x + 2*z' failed";
13.153 +(**}*)
13.154 +(*Makarius.1003
13.155 +ML {* @{term "2::int"} *}
13.156 +
13.157 +term "(1.24444) :: real"
13.158 +
13.159 +ML {* numbers_to_string @{term "%x. (-9993::int) + x + 1"} *}
13.160 +*)
13.161 +
13.162 +
13.163 +"----------- uminus_to_string ------------------------------------";
13.164 +"----------- uminus_to_string ------------------------------------";
13.165 +"----------- uminus_to_string ------------------------------------";
13.166 +(*ML {*)
13.167 +val t1 = numbers_to_string @{term "-2::real"};
13.168 +val t2 = numbers_to_string @{term "- 2::real"};
13.169 +if uminus_to_string t2 = t1 then ()
13.170 +else error "term_G.sml diff.behav. in uminus_to_string";
13.171 +(*}*)
14.1 --- a/test/Tools/isac/ProgLang/term_G.sml Mon Sep 13 18:37:16 2010 +0200
14.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
14.3 @@ -1,168 +0,0 @@
14.4 -(* tests on Scripts/term_G.sml
14.5 - author: Walther Neuper
14.6 - 051006,
14.7 - (c) due to copyright terms
14.8 -
14.9 -use"../smltest/Scripts/term_G.sml";
14.10 -use"term_G.sml";
14.11 -*)
14.12 -
14.13 -"-----------------------------------------------------------------";
14.14 -"table of contents -----------------------------------------------";
14.15 -"-----------------------------------------------------------------";
14.16 -"----------- inst_bdv --------------------------------------------";
14.17 -"----------- subst_atomic_all ------------------------------------";
14.18 -"----------- Pattern.match ---------------------------------------";
14.19 -"----------- fun matches -----------------------------------------";
14.20 -"------------parse------------------------------------------------";
14.21 -"----------- uminus_to_string ------------------------------------";
14.22 -"-----------------------------------------------------------------";
14.23 -"-----------------------------------------------------------------";
14.24 -
14.25 -
14.26 -"----------- inst_bdv --------------------------------------------";
14.27 -"----------- inst_bdv --------------------------------------------";
14.28 -"----------- inst_bdv --------------------------------------------";
14.29 -if string_of_thm (num_str @{thm d1_isolate_add2}) =
14.30 - "\"~ ?bdv occurs_in ?a ==> (?a + ?bdv = 0) = (?bdv = -1 * ?a)\"" then ()
14.31 -else raise error "term_G.sml d1_isolate_add2";
14.32 -val subst = [(str2term "bdv", str2term "x")];
14.33 -val t = (norm o #prop o rep_thm) (num_str @{thm d1_isolate_add2});
14.34 -val t' = inst_bdv subst t;
14.35 -if term2str t' = "~ x occurs_in ?a ==> (?a + x = 0) = (x = -1 * ?a)" then ()
14.36 -else raise error "term_G.sml inst_bdv 1";
14.37 -
14.38 -if string_of_thm (num_str @{thm separate_bdvs_add}) =
14.39 - "\"[] from_ [?bdv_1.0, ?bdv_2.0, ?bdv_3.0, ?bdv_4.0] occur_exactly_in ?a\n\
14.40 - \ ==> (?a + ?b = ?c) = (?b = ?c + -1 * ?a)\"" then ()
14.41 -else raise error "term_G.sml separate_bdvs_add";
14.42 -val subst = [(str2term"bdv_1",str2term"c"),
14.43 - (str2term"bdv_2",str2term"c_2"),
14.44 - (str2term"bdv_3",str2term"c_3"),
14.45 - (str2term"bdv_4",str2term"c_4")];
14.46 -val t = (norm o #prop o rep_thm) (num_str @{thm separate_bdvs_add});
14.47 -val t' = inst_bdv subst t;
14.48 -if term2str t' = "[] from_ [c, c_2, c_3, c_4] occur_exactly_in ?a\n\
14.49 - \==> (?a + ?b = ?c) = (?b = ?c + -1 * ?a)" then ()
14.50 -else raise error "term_G.sml inst_bdv 2";
14.51 -
14.52 -
14.53 -"----------- subst_atomic_all ------------------------------------";
14.54 -"----------- subst_atomic_all ------------------------------------";
14.55 -"----------- subst_atomic_all ------------------------------------";
14.56 -val t = str2term"(tl vs_) from_ vs_ occur_exactly_in (nth_ 1(es_::bool list))";
14.57 -val env = [(str2term"vs_::real list",str2term"[c, c_2]"),
14.58 - (str2term"es_::bool list",str2term"[c_2=0, c+c_2=1]")];
14.59 -val (all_Free_subst, t') = subst_atomic_all env t;
14.60 -if all_Free_subst andalso
14.61 - term2str t' = "tl [c, c_2] from_ [c, c_2] occur_exactly_in nth_ 1 [c_2 = 0, c + c_2 = 1]" then ()
14.62 -else raise error "term_G.sml subst_atomic_all should be 'true'";
14.63 -
14.64 -
14.65 -val (all_Free_subst, t') = subst_atomic_all (tl env) t;
14.66 -if not all_Free_subst andalso
14.67 - term2str t' = "tl vs_ from_ vs_ occur_exactly_in nth_ 1 [c_2 = 0, c + c_2 = 1]" then ()
14.68 -else raise error "term_G.sml subst_atomic_all should be 'false'";
14.69 -
14.70 -
14.71 -"----------- Pattern.match ---------------------------------------";
14.72 -"----------- Pattern.match ---------------------------------------";
14.73 -"----------- Pattern.match ---------------------------------------";
14.74 -val t = (term_of o the o (parse thy)) "3 * x^^^2 = 1";
14.75 -val pat = (free2var o term_of o the o (parse thy)) "a * b^^^2 = c";
14.76 -(* !^^^^^^^^!... necessary for Pattern.match*)
14.77 -val insts = Pattern.match (Sign.tsig_of (sign_of thy)) (pat, t);
14.78 -(*val insts =
14.79 - ([],
14.80 - [(("c",0),Free ("1","RealDef.real")),(("b",0),Free ("x","RealDef.real")),
14.81 - (("a",0),Free ("3","RealDef.real"))])
14.82 - : (indexname * typ) list * (indexname * term) list*)
14.83 -
14.84 -"----- throws exn MATCH...";
14.85 -val t = str2term "x";
14.86 -(Pattern.match (Sign.tsig_of (sign_of thy)) (pat, t))
14.87 -handle MATCH => ([(* (Term.indexname * Term.typ) *)],
14.88 - [(* (Term.indexname * Term.term) *)]);
14.89 -Pattern.MATCH;
14.90 -
14.91 -(*ML {**)
14.92 -val thy = @{theory "Complex_Main"};
14.93 -val PARSE = Syntax.read_term_global thy;
14.94 -val (pa, tm) = (PARSE "a + b::real", PARSE "x + 2*z::real");
14.95 -"-------";
14.96 -val (tye, tme) =
14.97 - (Vartab.empty : Type.tyenv, Vartab.empty : Envir.tenv);
14.98 -"-------";
14.99 -val (tye, tme) = Pattern.match thy (Logic.varify pa, tm) (Vartab.empty,
14.100 - Vartab.empty);
14.101 -"-------";
14.102 -val (tyenv, tenv) = Pattern.match thy (Logic.varify pa, tm)
14.103 - (Vartab.empty, Vartab.empty);
14.104 -Vartab.dest tenv;
14.105 -match thy tm (Logic.varify pa);
14.106 -
14.107 -(**}*)
14.108 -
14.109 -"----------- fun matches -----------------------------------------";
14.110 -"----------- fun matches -----------------------------------------";
14.111 -"----------- fun matches -----------------------------------------";
14.112 -(*smltest/IsacKnowledge/polyeq.sml:
14.113 - Where=[Correct "matches (?a = 0) (-8 - 2 * x + x ^^^ 2 = 0)"*)
14.114 -(*smltest/ME/ptyps.sml:
14.115 - |\nmatches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"],*)
14.116 -(*ML {**)
14.117 -val thy = @{theory "Complex_Main"};
14.118 -"----- test 1";
14.119 -val pa = Logic.varify @{term "a = (0::real)"};
14.120 -"----- test 1 true";
14.121 -val tm = @{term "-8 - 2 * x + x ^ 2 = (0::real)"};
14.122 -if matches thy tm pa then ()
14.123 - else error "term_G.sml diff.behav. in matches true";
14.124 -"----- test 2 false";
14.125 -val tm = @{term "-8 - 2 * x + x ^ 2 = (3::real)"};
14.126 -if matches thy tm pa then error "term_G.sml diff.behav. in matches false"
14.127 - else ();
14.128 -(**}*)
14.129 -
14.130 -"------------parse------------------------------------------------";
14.131 -"------------parse------------------------------------------------";
14.132 -"------------parse------------------------------------------------";
14.133 -(*ML {**)
14.134 -Toplevel.debug := true;
14.135 -(* literal types:
14.136 -PolyML.addPrettyPrinter
14.137 - (fn _ => fn _ => ml_pretty o Pretty.to_ML o raw_pp_typ);
14.138 -*)(* pretty types:
14.139 -PolyML.addPrettyPrinter
14.140 - (fn _ => fn _ => ml_pretty o Pretty.to_ML o Proof_Display.pp_typ Pure.thy);
14.141 -print_depth 99;
14.142 -*)
14.143 -val thy = @{theory "Complex_Main"};
14.144 -val str = "x + z";
14.145 -parse thy str;
14.146 -"---------------";
14.147 -val str = "x + 2*z";
14.148 -val t = (Syntax.read_term_global thy str);
14.149 -val t = numbers_to_string (Syntax.read_term_global thy str);
14.150 -val t = (typ_a2real o numbers_to_string) (Syntax.read_term_global thy str);
14.151 -cterm_of thy t;
14.152 -val t = (the (parse thy str)) handle _ => error "term_G.sml parsing 'x + 2*z' failed";
14.153 -(**}*)
14.154 -(*Makarius.1003
14.155 -ML {* @{term "2::int"} *}
14.156 -
14.157 -term "(1.24444) :: real"
14.158 -
14.159 -ML {* numbers_to_string @{term "%x. (-9993::int) + x + 1"} *}
14.160 -*)
14.161 -
14.162 -
14.163 -"----------- uminus_to_string ------------------------------------";
14.164 -"----------- uminus_to_string ------------------------------------";
14.165 -"----------- uminus_to_string ------------------------------------";
14.166 -(*ML {*)
14.167 -val t1 = numbers_to_string @{term "-2::real"};
14.168 -val t2 = numbers_to_string @{term "- 2::real"};
14.169 -if uminus_to_string t2 = t1 then ()
14.170 -else error "term_G.sml diff.behav. in uminus_to_string";
14.171 -(*}*)
15.1 --- a/test/Tools/isac/Run_Tests.thy Mon Sep 13 18:37:16 2010 +0200
15.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
15.3 @@ -1,11 +0,0 @@
15.4 -(*
15.5 -$ cd /usr/local/isabisac/test/Tools/isac
15.6 -$ /usr/local/isabisac/bin/isabelle emacs Run_Tests.thy &
15.7 -
15.8 -*)
15.9 -
15.10 -theory Run_Tests imports Main begin
15.11 -
15.12 -use "ProgLang/term.sml"
15.13 -
15.14 -end
16.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
16.2 +++ b/test/Tools/isac/Test_Isac.thy Tue Sep 14 12:12:42 2010 +0200
16.3 @@ -0,0 +1,111 @@
16.4 +(* Title Run_Tests on isac
16.5 +$ cd /usr/local/isabisac/test/Tools/isac
16.6 +$ /usr/local/isabisac/bin/isabelle emacs Run_Tests.thy &
16.7 +
16.8 +was sml/RTEST-root.sml in isac-2002
16.9 +*)
16.10 +
16.11 +theory Test_Isac imports Isac begin
16.12 +
16.13 +ML{* writeln "**** run the tests **************************************" *};
16.14 +(*
16.15 +cd "systest";
16.16 +(*+ check kbtest/diffapp.sml for additional items in met-model*)
16.17 + use"root-equ.sml";
16.18 + use"script.sml";
16.19 + (* use"script_if.sml"; WN03 missing: is_rootequation_in*)
16.20 + use"scriptnew.sml";
16.21 + use"subp-rooteq.sml";
16.22 + use"tacis.sml";
16.23 + use"interface-xml.sml";
16.24 + (* use"testdaten.sml"; no update after dropping 'errorBound'*)
16.25 + cd "../..";
16.26 +*)
16.27 +ML{* writeln "**** run systests complete ******************************" *};
16.28 +(*
16.29 +cd"smltest/Scripts";
16.30 + use"calculate-float.sml";
16.31 + use"calculate.sml";
16.32 + use"listg.sml";
16.33 + use"rewrite.sml";
16.34 + use"scrtools.sml";
16.35 + use"term.sml";
16.36 + use"tools.sml";
16.37 + cd "../..";
16.38 +cd"smltest/ME";
16.39 + use"ctree.sml";
16.40 +*)
16.41 +use "Interpret/calchead.sml"
16.42 +(*
16.43 + use"calchead.sml";
16.44 + use"rewtools.sml";
16.45 + use"solve.sml"; (*detailrls can notyet ackn. 'Rewrite_Set "cancel"' *);
16.46 + use"inform.sml";
16.47 + use"me.sml";
16.48 + use"ptyps.sml";
16.49 + cd "../..";
16.50 +cd"smltest/xmlsrc";
16.51 + use"datatypes.sml";
16.52 + use"pbl-met-hierarchy.sml";
16.53 + use"thy-hierarchy.sml";
16.54 + cd "../..";
16.55 +cd"smltest/FE-interface";
16.56 + use"interface.sml";
16.57 + cd "../..";
16.58 +*)
16.59 +ML{* writeln "**** run tests on math-engine complete ******************" *};
16.60 +(*
16.61 +cd"smltest/IsacKnowledge";
16.62 + use"atools.sml";
16.63 + use"complex.sml";
16.64 + use"diff.sml";
16.65 + use"diffapp.sml";
16.66 + use"integrate.sml";
16.67 + use"equation.sml";
16.68 + (*use"inssort.sml"; problems with recdef in Isabelle2002*)
16.69 + use"logexp.sml";
16.70 + use"poly.sml";
16.71 + use"polyminus.sml";
16.72 + use"polyeq.sml"; (*TODO 31.b, n1., 44.a, 1.a~, 1.b (all'expanded')WN
16.73 + ? also check others without check 'diff.behav.'*);
16.74 + use"rateq.sml";
16.75 + use"rational.sml" (*TODO add_fractions_p throws overflow-exn WN*);
16.76 + use"rlang.sml"; (*WN.12.6.03: for TODOs search 'writeln',
16.77 + for simplification search MG
16.78 + erls: 98a(1) 104a(1) 104a(2) 68a *);
16.79 + use"root.sml";
16.80 + use"rooteq.sml";
16.81 + use"rootrateq.sml";
16.82 + use"termorder.sml";
16.83 + use"trig.sml";
16.84 + use"vect.sml";
16.85 + use"wn.sml";
16.86 + use"eqsystem.sml";
16.87 + use"biegelinie.sml";
16.88 + use"algein.sml";
16.89 + cd "../..";
16.90 +*)
16.91 +ML{* writeln "**** run tests on IsacKnowledge complete ****************" *};
16.92 +(*
16.93 +val path = "/home/neuper/proto2/testsml2xml/";
16.94 +pbl_hierarchy2file (path ^ "pbl/");
16.95 +pbls2file (path ^ "pbl/");
16.96 +met_hierarchy2file (path ^ "met/");
16.97 +mets2file (path ^ "met/");
16.98 +thy_hierarchy2file (path ^ "thy/");
16.99 +thes2file (path ^ "thy/");
16.100 +cd"sml";
16.101 +*)
16.102 +ML{* writeln "**** tested creation of xmldata *************************" *};
16.103 +
16.104 +ML{*states:=[];
16.105 + writeln "=========================================================";
16.106 +
16.107 + writeln "**** run systests complete ***************** re-organize!";
16.108 + writeln "**** run tests on math-engine complete ******************";
16.109 + writeln "**** run tests on IsacKnowledge complete ****************";
16.110 + writeln "**** build isac kernel + run tests complete *************";
16.111 + writeln "**** tested creation of xmldata *************************";
16.112 +*}
16.113 +
16.114 +end