1.1 --- a/test/Tools/isac/Knowledge/rlang.sml Sun Oct 09 06:53:03 2022 +0200
1.2 +++ b/test/Tools/isac/Knowledge/rlang.sml Sun Oct 09 07:44:22 2022 +0200
1.3 @@ -193,8 +193,8 @@
1.4 [ (bdv, v) ] make_ratpoly_in t;
1.5 if UnparseC.term t' = "3 / 5 * x" then () else error "rlang.sml: 1";
1.6
1.7 -val t = TermC.str2term "(3*x+5)/18 - x/2 - -(3*x - 2)/9 = 0";
1.8 -val subst = [(TermC.str2term "bdv", TermC.str2term "x")];
1.9 +val t = TermC.parse_test @{context} "(3*x+5)/18 - x/2 - -(3*x - 2)/9 = 0";
1.10 +val subst = [(TermC.parse_test @{context} "bdv", TermC.parse_test @{context} "x")];
1.11 val SOME (t',_) = rewrite_set_inst_ thy false subst make_ratpoly_in t;
1.12 if UnparseC.term t' = "1 / 18 = 0" then () else error "rlang.sml: 2";
1.13 (*WN---^ *)
1.14 @@ -226,8 +226,8 @@
1.15
1.16
1.17 (*WN---v *)
1.18 -val t = TermC.str2term "(17*x - 51)/9 - (-(13*x - 3)/6) + 11 - (9*x - 7)/4 = 0";
1.19 -val subst = [(TermC.str2term "bdv", TermC.str2term "x")];
1.20 +val t = TermC.parse_test @{context} "(17*x - 51)/9 - (-(13*x - 3)/6) + 11 - (9*x - 7)/4 = 0";
1.21 +val subst = [(TermC.parse_test @{context} "bdv", TermC.parse_test @{context} "x")];
1.22 val SOME (t',_) = rewrite_set_inst_ thy false subst make_ratpoly_in t;
1.23 UnparseC.term t';
1.24 if UnparseC.term t' = "79 / 12 + 65 / 36 * x = 0" then ()
1.25 @@ -338,14 +338,14 @@
1.26 | _ => error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 44a [x = 1]";
1.27
1.28 (*WN---v *)
1.29 -val t = TermC.str2term "(1/2 + (5*x)/2) \<up> 2 - ((13*x)/2 - 5/2) \<up> 2 - (6*x) \<up> 2 + 29";
1.30 -val subst = [(TermC.str2term "bdv", TermC.str2term "x")];
1.31 +val t = TermC.parse_test @{context} "(1/2 + (5*x)/2) \<up> 2 - ((13*x)/2 - 5/2) \<up> 2 - (6*x) \<up> 2 + 29";
1.32 +val subst = [(TermC.parse_test @{context} "bdv", TermC.parse_test @{context} "x")];
1.33 val SOME (t',_) = rewrite_set_inst_ thy false subst make_ratpoly_in t;
1.34 if UnparseC.term t' = "23 + 35 * x + -72 * x \<up> 2" then ()
1.35 else error "rlang.sml: 4";
1.36
1.37 -val t = TermC.str2term "(1/2 + (5*x)/2) \<up> 2 - ((13*x)/2 - 5/2) \<up> 2 + (6*x) \<up> 2 - 29";
1.38 -val subst = [(TermC.str2term "bdv", TermC.str2term "x")];
1.39 +val t = TermC.parse_test @{context} "(1/2 + (5*x)/2) \<up> 2 - ((13*x)/2 - 5/2) \<up> 2 + (6*x) \<up> 2 - 29";
1.40 +val subst = [(TermC.parse_test @{context} "bdv", TermC.parse_test @{context} "x")];
1.41 val SOME (t',_) = rewrite_set_inst_ thy false subst make_ratpoly_in t;
1.42 if UnparseC.term t' = "-35 + 35 * x" then ()
1.43 else error "rlang.sml: 4.1";
1.44 @@ -486,7 +486,7 @@
1.45 "[v = (u * v0 + v0 * w + - 1 * f * w) / f]")) => ()
1.46 | _ => error "rlang.sml: diff.behav. in Schalk I s.89 Bsp 90a (1) [v=...]";
1.47 if Ctree.get_assumptions pt p =
1.48 - [TermC.str2term"(u * v0 + v0 * w + - 1 * f * w) / f + w ~= 0"] then ()
1.49 + [TermC.parse_test @{context}"(u * v0 + v0 * w + - 1 * f * w) / f + w ~= 0"] then ()
1.50 else error "rlang.sml: diff.behav. in I s.89 Bsp 90a (1) [v=...] asm";
1.51
1.52
1.53 @@ -530,8 +530,8 @@
1.54 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[w = (u * v0 + - 1 * f * v) / (f + - 1 * v0)]")) => ()
1.55 | _ => error "rlang.sml: diff.behav. in Schalk I Bsp 90a(2)";
1.56 if Ctree.get_assumptions pt p =
1.57 -[TermC.str2term"v + (u * v0 + - 1 * f * v) / (f + - 1 * v0) ~= 0",
1.58 - TermC.str2term"f + - 1 * v0 ~= 0"]
1.59 +[TermC.parse_test @{context}"v + (u * v0 + - 1 * f * v) / (f + - 1 * v0) ~= 0",
1.60 + TermC.parse_test @{context}"f + - 1 * v0 ~= 0"]
1.61 then writeln "asm should be simplified ???"
1.62 else error "rlang.sml: diff.behav. in Schalk I Bsp 90a(2) asm";
1.63
1.64 @@ -571,9 +571,9 @@
1.65 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.66 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[R1 = R * R2 / (R2 + - 1 * R)]")) => ()
1.67 | _ => error "rlang.sml: diff.behav. in 98a(1) [R1 = ...]";
1.68 -if Ctree.get_assumptions pt p = [TermC.str2term"R * R2 * R2 ~= (R2 + - 1 * R) * 0",
1.69 - TermC.str2term"R2 + - 1 * R ~= 0",
1.70 - TermC.str2term"R2 + - 1 * R ~= 0"]
1.71 +if Ctree.get_assumptions pt p = [TermC.parse_test @{context}"R * R2 * R2 ~= (R2 + - 1 * R) * 0",
1.72 + TermC.parse_test @{context}"R2 + - 1 * R ~= 0",
1.73 + TermC.parse_test @{context}"R2 + - 1 * R ~= 0"]
1.74 then writeln "asm should be simplified"
1.75 else error "rlang.sml: diff.behav. in 98a(1) asm";
1.76
1.77 @@ -602,7 +602,7 @@
1.78 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.79 case f of Form' (Test_Out.FormKF (_,_,0,_,"[p = y \<up> 2 / (2 * x)]")) => ()
1.80 | _ => error "rlang.sml: diff.behav. in Schalk I s.89 Bsp 104a (1) [p = y^2/(2*x)]";
1.81 -if Ctree.get_assumptions pt p = [TermC.str2term"- 2 * x ~= 0"]
1.82 +if Ctree.get_assumptions pt p = [TermC.parse_test @{context}"- 2 * x ~= 0"]
1.83 then writeln"should be x ~= 0\nshould be x ~= 0\nshould be x ~= 0\n"
1.84 else error "rlang.sml: diff.behav. in I s.89 Bsp 104a(1) asm";
1.85
1.86 @@ -632,8 +632,8 @@
1.87 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.88 case f of Form' (Test_Out.FormKF (_,_,0,_,"[y = sqrt (2 * p * x), y = - 1 * sqrt (2 * p * x)]")) => ()
1.89 | _ => error "rlang.sml: diff.behav. Schalk I s.89 Bsp 104a(2) [x = ]";
1.90 -if Ctree.get_assumptions pt p = [TermC.str2term"0 <= - 1 * (- 2 * p * x)",
1.91 - TermC.str2term"0 <= - 1 * (- 2 * p * x)"]
1.92 +if Ctree.get_assumptions pt p = [TermC.parse_test @{context}"0 <= - 1 * (- 2 * p * x)",
1.93 + TermC.parse_test @{context}"0 <= - 1 * (- 2 * p * x)"]
1.94 then writeln "asm should be simplified\nshould be simplified"
1.95 else error "rlang.sml: diff.behav. in I s.89 Bsp 104a(2) asm";
1.96
1.97 @@ -678,10 +678,10 @@
1.98 | _ => error "rlang.sml: diff.behav. in Schalk I s.89 Bsp 118a(2) [x = ]";
1.99 val asms = Ctree.get_assumptions pt p;
1.100 if asms =
1.101 - [TermC.str2term"0 * b \<up> 2 <= - 1 * (a \<up> 2 * y \<up> 2 + - 1 * a \<up> 2 * b \<up> 2)",
1.102 - TermC.str2term"b \<up> 2 ~= 0",
1.103 - TermC.str2term"0 * b \<up> 2 <= - 1 * (a \<up> 2 * y \<up> 2 + - 1 * a \<up> 2 * b \<up> 2)",
1.104 - TermC.str2term"b \<up> 2 ~= 0"] then writeln"should be simplified MG"
1.105 + [TermC.parse_test @{context}"0 * b \<up> 2 <= - 1 * (a \<up> 2 * y \<up> 2 + - 1 * a \<up> 2 * b \<up> 2)",
1.106 + TermC.parse_test @{context}"b \<up> 2 ~= 0",
1.107 + TermC.parse_test @{context}"0 * b \<up> 2 <= - 1 * (a \<up> 2 * y \<up> 2 + - 1 * a \<up> 2 * b \<up> 2)",
1.108 + TermC.parse_test @{context}"b \<up> 2 ~= 0"] then writeln"should be simplified MG"
1.109 else error "rlang.sml: diff.behav. in Schalk I s.89 Bsp 118a(2) asms";
1.110
1.111 (*----------------- Schalk I s.102 Bsp 268(1) ------------------------*)
1.112 @@ -709,7 +709,7 @@
1.113 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.114 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x2 =\n (- 2 * A + x1 * y2 + x3 * y1 + - 1 * x1 * y3 + - 1 * x3 * y2) /\n (y1 + - 1 * y3)]")) => ()
1.115 | _ => error "rlang.sml: diff.behav. Schalk I s.102 Bsp 268(1) [x2=...]";
1.116 -if Ctree.get_assumptions pt p = [TermC.str2term"y1 / 2 + - 1 * y3 / 2 ~= 0"] then ()
1.117 +if Ctree.get_assumptions pt p = [TermC.parse_test @{context}"y1 / 2 + - 1 * y3 / 2 ~= 0"] then ()
1.118 else error "rlang.sml: diff.behav. in I s.102 Bsp 268(1) asm";
1.119
1.120 (*-------------------- Schalk II ----------------------------*)
1.121 @@ -824,11 +824,11 @@
1.122 \0 <= 1 / 9]"
1.123 (*WN050916 before correction 'rewrite__set_ called with 'Rule_Set.Empty' for ..'
1.124 thus: maybe the rls for the asms is Rule_Set.Empty ??:
1.125 - [(TermC.str2term"0 <= (25 * (1 / 9) + - 1 * (16 + 49 * (1 / 9))) * -56", []),
1.126 - (TermC.str2term"9 ~= 0", []),
1.127 - (TermC.str2term"0 <= (-5 + 7 * sqrt (1 / 9) + 1) * 5", []),
1.128 - (TermC.str2term"9 ~= 0", []),
1.129 - (TermC.str2term"0 <= (25 * (1 / 9) + - 1 * (16 + 49 * (1 / 9))) * -56", [])]*)
1.130 + [(TermC.parse_test @{context}"0 <= (25 * (1 / 9) + - 1 * (16 + 49 * (1 / 9))) * -56", []),
1.131 + (TermC.parse_test @{context}"9 ~= 0", []),
1.132 + (TermC.parse_test @{context}"0 <= (-5 + 7 * sqrt (1 / 9) + 1) * 5", []),
1.133 + (TermC.parse_test @{context}"9 ~= 0", []),
1.134 + (TermC.parse_test @{context}"0 <= (25 * (1 / 9) + - 1 * (16 + 49 * (1 / 9))) * -56", [])]*)
1.135 then "should get True * False!!!"
1.136 else error "rlang.sml: diff.behav. in II 68a asms";
1.137
1.138 @@ -1329,7 +1329,7 @@
1.139 a * b / (a \<up> 2 + - 1 * b \<up> 2)"
1.140
1.141
1.142 -val t = TermC.str2term"(a + b * x) / (a + - 1 * (b * x)) + - 1 * (a + - 1 * (b * x)) / (a + b * x) =\n4 * a * b / (a \<up> 2 + - 1 * b \<up> 2)";
1.143 +val t = TermC.parse_test @{context}"(a + b * x) / (a + - 1 * (b * x)) + - 1 * (a + - 1 * (b * x)) / (a + b * x) =\n4 * a * b / (a \<up> 2 + - 1 * b \<up> 2)";
1.144 Rewrite.trace_on := false; (*true false*)
1.145 val SOME (t',asm) = rewrite_set_ thy false norm_Rational t;
1.146 UnparseC.term t';
1.147 @@ -1496,14 +1496,14 @@
1.148 "[x = (- 2 * a + 4 * b + sqrt (16 * a * b + 16 * b \<up> 2 + 4 * a \<up> 2)) / 4,\n x =\n (- 2 * a + 4 * b + - 1 * sqrt (16 * a * b + 16 * b \<up> 2 + 4 * a \<up> 2)) / 4]")) then writeln "simplify MG"
1.149 else error "rlang.sml: diff.behav. in II 62b [x=...]";
1.150 val asms = Ctree.get_assumptions pt p;
1.151 -if asms = [TermC.str2term"0 <= ((- 2 * a + 4 * b + sqrt (16 * a * b + 16 * b \<up> 2 + 4 * a \<up> 2)) / 4 + a) \<up> 2 + ((- 2 * a + 4 * b + sqrt (16 * a * b + 16 * b \<up> 2 + 4 * a \<up> 2)) / 4 - 2 * b) \<up> 2",
1.152 - TermC.str2term"0 <= a + 2 * b",
1.153 - TermC.str2term"8 * (-4 * a * b) <= (-4 * b + 2 * a) \<up> 2",
1.154 - TermC.str2term"8 * (-4 * a * b) <= (-4 * b + 2 * a) \<up> 2",
1.155 - TermC.str2term"0 <= ((- 2 * a + 4 * b + - 1 * sqrt (16 * a * b + 16 * b \<up> 2 + 4 * a \<up> 2)) / 4 + a) \<up> 2 + ((- 2 * a + 4 * b + - 1 * sqrt (16 * a * b + 16 * b \<up> 2 + 4 * a \<up> 2)) / 4 - 2 * b) \<up> 2",
1.156 - TermC.str2term"0 <= a + 2 * b",
1.157 - TermC.str2term"8 * (-4 * a * b) <= (-4 * b + 2 * a) \<up> 2",
1.158 - TermC.str2term"8 * (-4 * a * b) <= (-4 * b + 2 * a) \<up> 2"]
1.159 +if asms = [TermC.parse_test @{context}"0 <= ((- 2 * a + 4 * b + sqrt (16 * a * b + 16 * b \<up> 2 + 4 * a \<up> 2)) / 4 + a) \<up> 2 + ((- 2 * a + 4 * b + sqrt (16 * a * b + 16 * b \<up> 2 + 4 * a \<up> 2)) / 4 - 2 * b) \<up> 2",
1.160 + TermC.parse_test @{context}"0 <= a + 2 * b",
1.161 + TermC.parse_test @{context}"8 * (-4 * a * b) <= (-4 * b + 2 * a) \<up> 2",
1.162 + TermC.parse_test @{context}"8 * (-4 * a * b) <= (-4 * b + 2 * a) \<up> 2",
1.163 + TermC.parse_test @{context}"0 <= ((- 2 * a + 4 * b + - 1 * sqrt (16 * a * b + 16 * b \<up> 2 + 4 * a \<up> 2)) / 4 + a) \<up> 2 + ((- 2 * a + 4 * b + - 1 * sqrt (16 * a * b + 16 * b \<up> 2 + 4 * a \<up> 2)) / 4 - 2 * b) \<up> 2",
1.164 + TermC.parse_test @{context}"0 <= a + 2 * b",
1.165 + TermC.parse_test @{context}"8 * (-4 * a * b) <= (-4 * b + 2 * a) \<up> 2",
1.166 + TermC.parse_test @{context}"8 * (-4 * a * b) <= (-4 * b + 2 * a) \<up> 2"]
1.167 then writeln "should be simplified MG"
1.168 else error "rlang.sml: diff.behav. in II 62b asms";
1.169
1.170 @@ -1523,8 +1523,8 @@
1.171 (*
1.172 val f = Form' (Test_Out.FormKF (~1,EdUndef,1,Nundef,"(2 * x + 1) * x \<up> 2 = 0"))
1.173 normiert nicht ... korr.WN:
1.174 -val t = TermC.str2term "(2*x+1)*x \<up> 2 = 0";
1.175 -val subst = [(TermC.str2term "bdv", TermC.str2term "x")];
1.176 +val t = TermC.parse_test @{context} "(2*x+1)*x \<up> 2 = 0";
1.177 +val subst = [(TermC.parse_test @{context} "bdv", TermC.parse_test @{context} "x")];
1.178 val SOME (t',_) = rewrite_set_inst_ thy false subst make_ratpoly_in t;
1.179 if UnparseC.term t' = "x \<up> 2 + 2 * x \<up> 3 = 0" then ()
1.180 else error "rlang.sml: 7";
1.181 @@ -1547,7 +1547,7 @@
1.182
1.183 (*------------------------------vvv-Rewrite_Set "rat_eliminate"---------
1.184 > Rewrite.trace_on:=true; (*true false*)
1.185 -> val t = TermC.str2term
1.186 +> val t = TermC.parse_test @{context}
1.187 "(3 + - 1 * x + 1 * x \<up> 2) / (9 * x + -6 * x \<up> 2 + 1 * x \<up> 3) = 1 / x";
1.188 > val SOME (t',asm) =
1.189 rewrite_ thy dummy_ord rateq_erls true rat_mult_denominator_both t;
1.190 @@ -1595,8 +1595,8 @@
1.191 then writeln"simplify result\nsimplify result\nsimplify result"
1.192 else error "rlang.sml: diff.behav. in Pythagoras";
1.193 val asms = Ctree.get_assumptions pt p;
1.194 -(*if asms = [TermC.str2term"0 <= -4 * (b \<up> 2 / 4 + -4 * r \<up> 2 / 4)",
1.195 - TermC.str2term"0 <= -4 * (b \<up> 2 / 4 + -4 * r \<up> 2 / 4)"]*)
1.196 +(*if asms = [TermC.parse_test @{context}"0 <= -4 * (b \<up> 2 / 4 + -4 * r \<up> 2 / 4)",
1.197 + TermC.parse_test @{context}"0 <= -4 * (b \<up> 2 / 4 + -4 * r \<up> 2 / 4)"]*)
1.198 if UnparseC.terms (*WN1104changed*) asms =
1.199 "[0 <= -4 * (b \<up> 2 / 4 + - 1 * r \<up> 2 / 1),\
1.200 \0 <= -4 * (b \<up> 2 / 4 + - 1 * r \<up> 2 / 1)]"