1.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml Tue May 19 12:33:35 2020 +0200
1.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml Wed May 20 12:52:09 2020 +0200
1.3 @@ -108,8 +108,8 @@
1.4 "----------- test matching problems --------------------------0---";
1.5 "----------- test matching problems --------------------------0---";
1.6 "----------- test matching problems --------------------------0---";
1.7 -val fmz = ["equality (-8 - 2*x + x^^^2 = 0)", "solveFor x","solutions L"];
1.8 -if M_Match.match_pbl fmz (Problem.from_store ["expanded","univariate","equation"]) =
1.9 +val fmz = ["equality (-8 - 2*x + x^^^2 = 0)", "solveFor x", "solutions L"];
1.10 +if M_Match.match_pbl fmz (Problem.from_store ["expanded", "univariate", "equation"]) =
1.11 M_Match.Matches' {Find = [Correct "solutions L"],
1.12 With = [],
1.13 Given = [Correct "equality (-8 - 2 * x + x ^^^ 2 = 0)", Correct "solveFor x"],
1.14 @@ -118,7 +118,7 @@
1.15 Relate = []}
1.16 then () else error "M_Match.match_pbl [expanded,univariate,equation]";
1.17
1.18 -if M_Match.match_pbl fmz (Problem.from_store ["degree_2","expanded","univariate","equation"]) =
1.19 +if M_Match.match_pbl fmz (Problem.from_store ["degree_2", "expanded", "univariate", "equation"]) =
1.20 M_Match.Matches' {Find = [Correct "solutions L"],
1.21 With = [],
1.22 Given = [Correct "equality (-8 - 2 * x + x ^^^ 2 = 0)", Correct "solveFor x"],
1.23 @@ -140,7 +140,7 @@
1.24 UnparseC.term t;
1.25 "a * b + (-1 * (a * x) + (-1 * (b * x) + x ^^^ 2)) = 0";
1.26 val SOME (t,_) =
1.27 - rewrite_set_inst_ thy Poly_erls false [("bdv","a")] make_polynomial_in t;
1.28 + rewrite_set_inst_ thy Poly_erls false [("bdv", "a")] make_polynomial_in t;
1.29 UnparseC.term t;
1.30 "x ^^^ 2 + (-1 * (b * x) + (-1 * (x * a) + b * a)) = 0";
1.31 (* bei Verwendung von "size_of-term" nach MG :*)
1.32 @@ -153,7 +153,7 @@
1.33 (* "x ^^^ 2 + -1 * b * x + b * a + -1 * x * a = 0" !!! *)
1.34
1.35 val SOME (t,_) =
1.36 - rewrite_set_inst_ thy Poly_erls false [("bdv","a")] make_polynomial_in t;
1.37 + rewrite_set_inst_ thy Poly_erls false [("bdv", "a")] make_polynomial_in t;
1.38 UnparseC.term t;
1.39 "x ^^^ 2 + (-1 * (b * x) + a * (b + -1 * x)) = 0";
1.40 (*da sind wir fast am Ziel: make_polynomial_in 'a' sollte ergeben
1.41 @@ -297,8 +297,8 @@
1.42 "----------- lin.eq degree_0 -------------------------------------";
1.43 "----- d0_false ------";
1.44 val fmz = ["equality (1 = (0::real))", "solveFor x", "solutions L"];
1.45 -val (dI',pI',mI') = ("PolyEq",["degree_0","polynomial","univariate","equation"],
1.46 - ["PolyEq","solve_d0_polyeq_equation"]);
1.47 +val (dI',pI',mI') = ("PolyEq",["degree_0", "polynomial", "univariate", "equation"],
1.48 + ["PolyEq", "solve_d0_polyeq_equation"]);
1.49 (*=== inhibit exn WN110914: declare_constraints doesnt work with ThmC.numerals_to_Free ========
1.50 TODO: change to "equality (x + -1*x = (0::real))"
1.51 and search for an appropriate problem and method.
1.52 @@ -314,9 +314,9 @@
1.53 | _ => error "polyeq.sml: diff.behav. in 1 = 0 -> []";
1.54
1.55 "----- d0_true ------";
1.56 -val fmz = ["equality (0 = (0::real))", "solveFor x","solutions L"];
1.57 -val (dI',pI',mI') = ("PolyEq",["degree_0","polynomial","univariate","equation"],
1.58 - ["PolyEq","solve_d0_polyeq_equation"]);
1.59 +val fmz = ["equality (0 = (0::real))", "solveFor x", "solutions L"];
1.60 +val (dI',pI',mI') = ("PolyEq",["degree_0", "polynomial", "univariate", "equation"],
1.61 + ["PolyEq", "solve_d0_polyeq_equation"]);
1.62 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.63 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.64 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.65 @@ -332,9 +332,9 @@
1.66 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
1.67 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
1.68 "----- d2_pqformula1 ------!!!!";
1.69 -val fmz = ["equality (-1/8 + (-1/4)*z + z^^^2 = (0::real))", "solveFor z","solutions L"];
1.70 +val fmz = ["equality (-1/8 + (-1/4)*z + z^^^2 = (0::real))", "solveFor z", "solutions L"];
1.71 val (dI',pI',mI') =
1.72 - ("Isac_Knowledge", ["pqFormula","degree_2","polynomial","univariate","equation"], ["no_met"]);
1.73 + ("Isac_Knowledge", ["pqFormula", "degree_2", "polynomial", "univariate", "equation"], ["no_met"]);
1.74 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.75 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.76 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.77 @@ -362,8 +362,8 @@
1.78 "----------- equality (2 +(-1)*x + x^^^2 = (0::real)) ----------------------------------------";
1.79 "----------- equality (2 +(-1)*x + x^^^2 = (0::real)) ----------------------------------------";
1.80 "----- d2_pqformula1_neg ------";
1.81 -val fmz = ["equality (2 +(-1)*x + x^^^2 = (0::real))", "solveFor x","solutions L"];
1.82 -val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_pq_equation"]);
1.83 +val fmz = ["equality (2 +(-1)*x + x^^^2 = (0::real))", "solveFor x", "solutions L"];
1.84 +val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_pq_equation"]);
1.85 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.86 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.87 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.88 @@ -379,7 +379,7 @@
1.89 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.90 val asm = Ctree.get_assumptions pt p;
1.91 if f2str f = "[]" andalso
1.92 - UnparseC.terms asm = "[\"lhs (2 + -1 * x + x ^^^ 2 = 0) is_poly_in x\"," ^
1.93 + UnparseC.terms asm = "[\"lhs (2 + -1 * x + x ^^^ 2 = 0) is_poly_in x\", " ^
1.94 "\"lhs (2 + -1 * x + x ^^^ 2 = 0) has_degree_in x = 2\"]" then ()
1.95 else error "polyeq.sml: diff.behav. in 2 +(-1)*x + x^^^2 = 0";
1.96
1.97 @@ -387,9 +387,9 @@
1.98 "----------- equality (-2 +(-1)*x + 1*x^^^2 = 0) ---------------------------------------------";
1.99 "----------- equality (-2 +(-1)*x + 1*x^^^2 = 0) ---------------------------------------------";
1.100 "----- d2_pqformula2 ------";
1.101 -val fmz = ["equality (-2 +(-1)*x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
1.102 -val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
1.103 - ["PolyEq","solve_d2_polyeq_pq_equation"]);
1.104 +val fmz = ["equality (-2 +(-1)*x + 1*x^^^2 = 0)", "solveFor x", "solutions L"];
1.105 +val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
1.106 + ["PolyEq", "solve_d2_polyeq_pq_equation"]);
1.107 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.108 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.109 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.110 @@ -409,9 +409,9 @@
1.111 "----------- equality (-2 + x + x^^^2 = 0) ---------------------------------------------------";
1.112 "----- d2_pqformula3 ------";
1.113 (*EP-9*)
1.114 -val fmz = ["equality (-2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
1.115 -val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
1.116 - ["PolyEq","solve_d2_polyeq_pq_equation"]);
1.117 +val fmz = ["equality (-2 + x + x^^^2 = 0)", "solveFor x", "solutions L"];
1.118 +val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
1.119 + ["PolyEq", "solve_d2_polyeq_pq_equation"]);
1.120 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.121 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.122 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.123 @@ -430,9 +430,9 @@
1.124 "----------- equality (2 + x + x^^^2 = 0) ----------------------------------------------------";
1.125 "----------- equality (2 + x + x^^^2 = 0) ----------------------------------------------------";
1.126 "----- d2_pqformula3_neg ------";
1.127 -val fmz = ["equality (2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
1.128 -val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
1.129 - ["PolyEq","solve_d2_polyeq_pq_equation"]);
1.130 +val fmz = ["equality (2 + x + x^^^2 = 0)", "solveFor x", "solutions L"];
1.131 +val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
1.132 + ["PolyEq", "solve_d2_polyeq_pq_equation"]);
1.133 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.134 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.135 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.136 @@ -450,9 +450,9 @@
1.137 "----------- equality (-2 + x + 1*x^^^2 = 0)) ------------------------------------------------";
1.138 "----------- equality (-2 + x + 1*x^^^2 = 0)) ------------------------------------------------";
1.139 "----- d2_pqformula4 ------";
1.140 -val fmz = ["equality (-2 + x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
1.141 -val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
1.142 - ["PolyEq","solve_d2_polyeq_pq_equation"]);
1.143 +val fmz = ["equality (-2 + x + 1*x^^^2 = 0)", "solveFor x", "solutions L"];
1.144 +val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
1.145 + ["PolyEq", "solve_d2_polyeq_pq_equation"]);
1.146 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.147 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.148 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.149 @@ -469,9 +469,9 @@
1.150 "----------- equality (1*x + x^^^2 = 0) ----------------------------------------------------";
1.151 "----------- equality (1*x + x^^^2 = 0) ----------------------------------------------------";
1.152 "----- d2_pqformula5 ------";
1.153 -val fmz = ["equality (1*x + x^^^2 = 0)", "solveFor x","solutions L"];
1.154 -val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
1.155 - ["PolyEq","solve_d2_polyeq_pq_equation"]);
1.156 +val fmz = ["equality (1*x + x^^^2 = 0)", "solveFor x", "solutions L"];
1.157 +val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
1.158 + ["PolyEq", "solve_d2_polyeq_pq_equation"]);
1.159 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.160 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.161 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.162 @@ -488,9 +488,9 @@
1.163 "----------- equality (1*x + 1*x^^^2 = 0) ----------------------------------------------------";
1.164 "----------- equality (1*x + 1*x^^^2 = 0) ----------------------------------------------------";
1.165 "----- d2_pqformula6 ------";
1.166 -val fmz = ["equality (1*x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
1.167 -val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
1.168 - ["PolyEq","solve_d2_polyeq_pq_equation"]);
1.169 +val fmz = ["equality (1*x + 1*x^^^2 = 0)", "solveFor x", "solutions L"];
1.170 +val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
1.171 + ["PolyEq", "solve_d2_polyeq_pq_equation"]);
1.172 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.173 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.174 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.175 @@ -508,9 +508,9 @@
1.176 "----------- equality (x + x^^^2 = 0) ------------------------------------------------------";
1.177 "----- d2_pqformula7 ------";
1.178 (*EP-10*)
1.179 -val fmz = ["equality ( x + x^^^2 = 0)", "solveFor x","solutions L"];
1.180 -val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
1.181 - ["PolyEq","solve_d2_polyeq_pq_equation"]);
1.182 +val fmz = ["equality ( x + x^^^2 = 0)", "solveFor x", "solutions L"];
1.183 +val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
1.184 + ["PolyEq", "solve_d2_polyeq_pq_equation"]);
1.185 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.186 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.187 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.188 @@ -527,9 +527,9 @@
1.189 "----------- equality (x + 1*x^^^2 = 0) ------------------------------------------------------";
1.190 "----------- equality (x + 1*x^^^2 = 0) ------------------------------------------------------";
1.191 "----- d2_pqformula8 ------";
1.192 -val fmz = ["equality (x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
1.193 -val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
1.194 - ["PolyEq","solve_d2_polyeq_pq_equation"]);
1.195 +val fmz = ["equality (x + 1*x^^^2 = 0)", "solveFor x", "solutions L"];
1.196 +val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
1.197 + ["PolyEq", "solve_d2_polyeq_pq_equation"]);
1.198 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.199 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.200 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.201 @@ -546,9 +546,9 @@
1.202 "----------- equality (-4 + x^^^2 = 0) -------------------------------------------------------";
1.203 "----------- equality (-4 + x^^^2 = 0) -------------------------------------------------------";
1.204 "----- d2_pqformula9 ------";
1.205 -val fmz = ["equality (-4 + x^^^2 = 0)", "solveFor x","solutions L"];
1.206 -val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
1.207 - ["PolyEq","solve_d2_polyeq_pq_equation"]);
1.208 +val fmz = ["equality (-4 + x^^^2 = 0)", "solveFor x", "solutions L"];
1.209 +val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
1.210 + ["PolyEq", "solve_d2_polyeq_pq_equation"]);
1.211 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.212 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.213 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.214 @@ -565,9 +565,9 @@
1.215 "----------- equality (4 + 1*x^^^2 = 0) -------------------------------------------------------";
1.216 "----------- equality (4 + 1*x^^^2 = 0) -------------------------------------------------------";
1.217 "----- d2_pqformula9_neg ------";
1.218 -val fmz = ["equality (4 + 1*x^^^2 = 0)", "solveFor x","solutions L"];
1.219 -val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
1.220 - ["PolyEq","solve_d2_polyeq_pq_equation"]);
1.221 +val fmz = ["equality (4 + 1*x^^^2 = 0)", "solveFor x", "solutions L"];
1.222 +val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
1.223 + ["PolyEq", "solve_d2_polyeq_pq_equation"]);
1.224 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.225 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.226 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.227 @@ -582,9 +582,9 @@
1.228 "-------------------- test thm's d2_abc_formulsxx[_neg]-----";
1.229 "-------------------- test thm's d2_abc_formulsxx[_neg]-----";
1.230 "-------------------- test thm's d2_abc_formulsxx[_neg]-----";
1.231 -val fmz = ["equality (-1 +(-1)*x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
1.232 -val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
1.233 - ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.234 +val fmz = ["equality (-1 +(-1)*x + 2*x^^^2 = 0)", "solveFor x", "solutions L"];
1.235 +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
1.236 + ["PolyEq", "solve_d2_polyeq_abc_equation"]);
1.237 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.238 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.239 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.240 @@ -599,9 +599,9 @@
1.241 "----------- equality (1 +(-1)*x + 2*x^^^2 = 0) ----------------------------------------------";
1.242 "----------- equality (1 +(-1)*x + 2*x^^^2 = 0) ----------------------------------------------";
1.243 "----------- equality (1 +(-1)*x + 2*x^^^2 = 0) ----------------------------------------------";
1.244 -val fmz = ["equality (1 +(-1)*x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
1.245 -val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
1.246 - ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.247 +val fmz = ["equality (1 +(-1)*x + 2*x^^^2 = 0)", "solveFor x", "solutions L"];
1.248 +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
1.249 + ["PolyEq", "solve_d2_polyeq_abc_equation"]);
1.250 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.251 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.252 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.253 @@ -619,9 +619,9 @@
1.254 "----------- equality (-1 + x + 2*x^^^2 = 0) -------------------------------------------------";
1.255 "----------- equality (-1 + x + 2*x^^^2 = 0) -------------------------------------------------";
1.256 (*EP-11*)
1.257 -val fmz = ["equality (-1 + x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
1.258 -val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
1.259 - ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.260 +val fmz = ["equality (-1 + x + 2*x^^^2 = 0)", "solveFor x", "solutions L"];
1.261 +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
1.262 + ["PolyEq", "solve_d2_polyeq_abc_equation"]);
1.263 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.264 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.265 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.266 @@ -639,9 +639,9 @@
1.267 "----------- equality (1 + x + 2*x^^^2 = 0) --------------------------------------------------";
1.268 "----------- equality (1 + x + 2*x^^^2 = 0) --------------------------------------------------";
1.269 "----------- equality (1 + x + 2*x^^^2 = 0) --------------------------------------------------";
1.270 -val fmz = ["equality (1 + x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
1.271 -val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
1.272 - ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.273 +val fmz = ["equality (1 + x + 2*x^^^2 = 0)", "solveFor x", "solutions L"];
1.274 +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
1.275 + ["PolyEq", "solve_d2_polyeq_abc_equation"]);
1.276 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.277 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.278 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.279 @@ -656,9 +656,9 @@
1.280 "TODO 1 + x + 2*x^^^2 = 0";
1.281
1.282
1.283 -val fmz = ["equality (-2 + 1*x + x^^^2 = 0)", "solveFor x","solutions L"];
1.284 -val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
1.285 - ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.286 +val fmz = ["equality (-2 + 1*x + x^^^2 = 0)", "solveFor x", "solutions L"];
1.287 +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
1.288 + ["PolyEq", "solve_d2_polyeq_abc_equation"]);
1.289 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.290 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.291 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.292 @@ -670,9 +670,9 @@
1.293 case f of Test_Out.FormKF "[x = 1, x = -2]" => ()
1.294 | _ => error "polyeq.sml: diff.behav. in -2 + 1*x + x^2 = 0 -> [x = 1, x = -2]";
1.295
1.296 -val fmz = ["equality ( 2 + 1*x + x^^^2 = 0)", "solveFor x","solutions L"];
1.297 -val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
1.298 - ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.299 +val fmz = ["equality ( 2 + 1*x + x^^^2 = 0)", "solveFor x", "solutions L"];
1.300 +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
1.301 + ["PolyEq", "solve_d2_polyeq_abc_equation"]);
1.302 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.303 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.304 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.305 @@ -686,9 +686,9 @@
1.306 "TODO 2 + 1*x + x^^^2 = 0";
1.307
1.308 (*EP-12*)
1.309 -val fmz = ["equality (-2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
1.310 -val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
1.311 - ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.312 +val fmz = ["equality (-2 + x + x^^^2 = 0)", "solveFor x", "solutions L"];
1.313 +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
1.314 + ["PolyEq", "solve_d2_polyeq_abc_equation"]);
1.315 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.316 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.317 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.318 @@ -700,9 +700,9 @@
1.319 case f of Test_Out.FormKF "[x = 1, x = -2]" => ()
1.320 | _ => error "polyeq.sml: diff.behav. in -2 + x + x^2 = 0 -> [x = 1, x = -2]";
1.321
1.322 -val fmz = ["equality ( 2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
1.323 -val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
1.324 - ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.325 +val fmz = ["equality ( 2 + x + x^^^2 = 0)", "solveFor x", "solutions L"];
1.326 +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
1.327 + ["PolyEq", "solve_d2_polyeq_abc_equation"]);
1.328 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.329 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.330 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.331 @@ -716,9 +716,9 @@
1.332 "TODO 2 + x + x^^^2 = 0";
1.333
1.334 (*EP-13*)
1.335 -val fmz = ["equality (-8 + 2*x^^^2 = 0)", "solveFor x","solutions L"];
1.336 -val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
1.337 - ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.338 +val fmz = ["equality (-8 + 2*x^^^2 = 0)", "solveFor x", "solutions L"];
1.339 +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
1.340 + ["PolyEq", "solve_d2_polyeq_abc_equation"]);
1.341 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.342 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.343 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.344 @@ -730,9 +730,9 @@
1.345 case f of Test_Out.FormKF "[x = 2, x = -2]" => ()
1.346 | _ => error "polyeq.sml: diff.behav. in -8 + 2*x^2 = 0 -> [x = 2, x = -2]";
1.347
1.348 -val fmz = ["equality ( 8+ 2*x^^^2 = 0)", "solveFor x","solutions L"];
1.349 -val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
1.350 - ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.351 +val fmz = ["equality ( 8+ 2*x^^^2 = 0)", "solveFor x", "solutions L"];
1.352 +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
1.353 + ["PolyEq", "solve_d2_polyeq_abc_equation"]);
1.354 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.355 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.356 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.357 @@ -745,8 +745,8 @@
1.358 "TODO 8+ 2*x^^^2 = 0";
1.359
1.360 (*EP-14*)
1.361 -val fmz = ["equality (-4 + x^^^2 = 0)", "solveFor x","solutions L"];
1.362 -val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.363 +val fmz = ["equality (-4 + x^^^2 = 0)", "solveFor x", "solutions L"];
1.364 +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_abc_equation"]);
1.365 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.366 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.367 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.368 @@ -759,8 +759,8 @@
1.369 | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = -2]";
1.370
1.371
1.372 -val fmz = ["equality ( 4+ x^^^2 = 0)", "solveFor x","solutions L"];
1.373 -val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.374 +val fmz = ["equality ( 4+ x^^^2 = 0)", "solveFor x", "solutions L"];
1.375 +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_abc_equation"]);
1.376 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.377 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.378 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.379 @@ -773,9 +773,9 @@
1.380 "TODO 4+ x^^^2 = 0";
1.381
1.382 (*EP-15*)
1.383 -val fmz = ["equality (2*x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
1.384 -val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
1.385 - ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.386 +val fmz = ["equality (2*x + 2*x^^^2 = 0)", "solveFor x", "solutions L"];
1.387 +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
1.388 + ["PolyEq", "solve_d2_polyeq_abc_equation"]);
1.389 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.390 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.391 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.392 @@ -787,9 +787,9 @@
1.393 case f of Test_Out.FormKF "[x = 0, x = -1]" => ()
1.394 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
1.395
1.396 -val fmz = ["equality (1*x + x^^^2 = 0)", "solveFor x","solutions L"];
1.397 -val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
1.398 - ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.399 +val fmz = ["equality (1*x + x^^^2 = 0)", "solveFor x", "solutions L"];
1.400 +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
1.401 + ["PolyEq", "solve_d2_polyeq_abc_equation"]);
1.402 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.403 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.404 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.405 @@ -802,9 +802,9 @@
1.406 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
1.407
1.408 (*EP-16*)
1.409 -val fmz = ["equality (x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
1.410 -val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
1.411 - ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.412 +val fmz = ["equality (x + 2*x^^^2 = 0)", "solveFor x", "solutions L"];
1.413 +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
1.414 + ["PolyEq", "solve_d2_polyeq_abc_equation"]);
1.415 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.416 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.417 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.418 @@ -817,9 +817,9 @@
1.419 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1 / 2]";
1.420
1.421 (*EP-//*)
1.422 -val fmz = ["equality (x + x^^^2 = 0)", "solveFor x","solutions L"];
1.423 -val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
1.424 - ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.425 +val fmz = ["equality (x + x^^^2 = 0)", "solveFor x", "solutions L"];
1.426 +val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
1.427 + ["PolyEq", "solve_d2_polyeq_abc_equation"]);
1.428 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.429 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.430 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.431 @@ -841,17 +841,17 @@
1.432 see also --- (-8 - 2*x + x^^^2 = 0), by rewriting --- below
1.433 *)
1.434 val fmz = ["equality (-8 - 2*x + x^^^2 = 0)", (*Schalk 2, S.67 Nr.31.b*)
1.435 - "solveFor x","solutions L"];
1.436 + "solveFor x", "solutions L"];
1.437 val (dI',pI',mI') =
1.438 - ("PolyEq",["degree_2","expanded","univariate","equation"],
1.439 - ["PolyEq","complete_square"]);
1.440 + ("PolyEq",["degree_2", "expanded", "univariate", "equation"],
1.441 + ["PolyEq", "complete_square"]);
1.442 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.443 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.444 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.445 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.446
1.447 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.448 -(*Apply_Method ("PolyEq","complete_square")*)
1.449 +(*Apply_Method ("PolyEq", "complete_square")*)
1.450 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.451 (*"-8 - 2 * x + x ^^^ 2 = 0", nxt = Rewrite_Set_Inst ... "complete_square*)
1.452 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.453 @@ -948,10 +948,10 @@
1.454 else error "polyeq.sml: diff.behav. in 'rewrite_set_.. PolyEq_erls";*)
1.455 (* *)
1.456 val fmz = ["equality (3 - 10*x + 3*x^^^2 = 0)",
1.457 - "solveFor x","solutions L"];
1.458 + "solveFor x", "solutions L"];
1.459 val (dI',pI',mI') =
1.460 - ("PolyEq",["degree_2","expanded","univariate","equation"],
1.461 - ["PolyEq","complete_square"]);
1.462 + ("PolyEq",["degree_2", "expanded", "univariate", "equation"],
1.463 + ["PolyEq", "complete_square"]);
1.464 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.465 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.466 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.467 @@ -960,17 +960,17 @@
1.468 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.469 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.470 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.471 - (*Apply_Method ("PolyEq","complete_square")*)
1.472 + (*Apply_Method ("PolyEq", "complete_square")*)
1.473 val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
1.474
1.475 "----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
1.476 "----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
1.477 "----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
1.478 val fmz = ["equality (-16 + 4*x + 2*x^^^2 = 0)",
1.479 - "solveFor x","solutions L"];
1.480 + "solveFor x", "solutions L"];
1.481 val (dI',pI',mI') =
1.482 - ("PolyEq",["degree_2","expanded","univariate","equation"],
1.483 - ["PolyEq","complete_square"]);
1.484 + ("PolyEq",["degree_2", "expanded", "univariate", "equation"],
1.485 + ["PolyEq", "complete_square"]);
1.486 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.487 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.488 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.489 @@ -979,7 +979,7 @@
1.490 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.491 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.492 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.493 - (*Apply_Method ("PolyEq","complete_square")*)
1.494 + (*Apply_Method ("PolyEq", "complete_square")*)
1.495 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.496 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.497 val (p,_,f,nxt,_,pt) = me nxt p [] pt;