1.1 --- a/test/Tools/isac/Interpret/error-pattern.sml Tue Jul 13 15:28:43 2021 +0200
1.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml Thu Jul 15 14:10:18 2021 +0200
1.3 @@ -59,25 +59,25 @@
1.4 Iterator 1; moveActiveRoot 1;
1.5 autoCalculate 1 CompleteCalcHead;
1.6 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
1.7 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
1.8 + autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + - 1 * 2 = 0*);
1.9
1.10 - appendFormula 1 "-2 * 1 + (1 + x) = 0" (*|> Future.join*); refFormula 1 (get_pos 1 1);
1.11 + appendFormula 1 "- 2 * 1 + (1 + x) = 0" (*|> Future.join*); refFormula 1 (get_pos 1 1);
1.12 val ((pt,_),_) = get_calc 1;
1.13 val str = pr_ctree pr_short pt;
1.14 if str =
1.15 (". ----- pblobj -----\n" ^
1.16 "1. x + 1 = 2\n" ^
1.17 -"2. x + 1 + -1 * 2 = 0\n" ^
1.18 -"2.1. x + 1 + -1 * 2 = 0\n" ^
1.19 -"2.2. 1 + x + -1 * 2 = 0\n" ^
1.20 -"2.3. 1 + (x + -1 * 2) = 0\n" ^
1.21 -"2.4. 1 + (x + -2) = 0\n" ^
1.22 -"2.5. 1 + (x + -2 * 1) = 0\n" ^
1.23 -"2.6. 1 + x + -2 * 1 = 0\n" ) then ()
1.24 +"2. x + 1 + - 1 * 2 = 0\n" ^
1.25 +"2.1. x + 1 + - 1 * 2 = 0\n" ^
1.26 +"2.2. 1 + x + - 1 * 2 = 0\n" ^
1.27 +"2.3. 1 + (x + - 1 * 2) = 0\n" ^
1.28 +"2.4. 1 + (x + - 2) = 0\n" ^
1.29 +"2.5. 1 + (x + - 2 * 1) = 0\n" ^
1.30 +"2.6. 1 + x + - 2 * 1 = 0\n" ) then ()
1.31 else error "inform.sml: diff.behav.appendFormula: on Res + equ 1";
1.32
1.33 moveDown 1 ([ ],Pbl); refFormula 1 ([1],Frm); (*x + 1 = 2*)
1.34 - moveDown 1 ([1],Frm); refFormula 1 ([1],Res); (*x + 1 + -1 * 2 = 0*)
1.35 + moveDown 1 ([1],Frm); refFormula 1 ([1],Res); (*x + 1 + - 1 * 2 = 0*)
1.36
1.37 (*the seven steps of detailed derivation*)
1.38 moveDown 1 ([1 ],Res); refFormula 1 ([2,1],Frm);
1.39 @@ -88,7 +88,7 @@
1.40 moveDown 1 ([2,4],Res); refFormula 1 ([2,5],Res);
1.41 moveDown 1 ([2,5],Res); refFormula 1 ([2,6],Res);
1.42 val ((pt,_),_) = get_calc 1;
1.43 - if "-2 * 1 + (1 + x) = 0" = UnparseC.term (fst (get_obj g_result pt [2,6])) then()
1.44 + if "- 2 * 1 + (1 + x) = 0" = UnparseC.term (fst (get_obj g_result pt [2,6])) then()
1.45 else error "inform.sml: diff.behav.appendFormula: on Res + equ 2";
1.46
1.47 fetchProposedTactic 1; (*takes Iterator 1 _1_*)
1.48 @@ -119,13 +119,13 @@
1.49 val fod = Derive.do_one (@{theory "Isac_Knowledge"}) Atools_erls
1.50 ((#rules o Rule_Set.rep) Test_simplify)
1.51 (sqrt_right false (@{theory "Pure"})) NONE
1.52 - (TermC.str2term "x + 1 + -1 * 2 = 0");
1.53 + (TermC.str2term "x + 1 + - 1 * 2 = 0");
1.54 (writeln o Derive.trtas2str) fod;
1.55
1.56 val ifod = Derive.do_one (@{theory "Isac_Knowledge"}) Atools_erls
1.57 ((#rules o Rule_Set.rep) Test_simplify)
1.58 (sqrt_right false (@{theory "Pure"})) NONE
1.59 - (TermC.str2term "-2 * 1 + (1 + x) = 0");
1.60 + (TermC.str2term "- 2 * 1 + (1 + x) = 0");
1.61 (writeln o Derive.trtas2str) ifod;
1.62 fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1 = t2;
1.63 val (fod', rifod') = dropwhile' equal (rev fod) (rev ifod);
1.64 @@ -144,7 +144,7 @@
1.65 Iterator 1; moveActiveRoot 1;
1.66 autoCalculate 1 CompleteCalcHead;
1.67 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1) (*x + 1 = 2*);
1.68 - appendFormula 1 "2+ -1 + x = 2" (*|> Future.join*); refFormula 1 (get_pos 1 1);
1.69 + appendFormula 1 "2+ - 1 + x = 2" (*|> Future.join*); refFormula 1 (get_pos 1 1);
1.70
1.71 moveDown 1 ([],Pbl); refFormula 1 ([1],Frm) (*x + 1 = 2*);
1.72
1.73 @@ -156,7 +156,7 @@
1.74 moveDown 1 ([1,4],Res); refFormula 1 ([1,5],Res);
1.75 moveDown 1 ([1,5],Res); refFormula 1 ([1,6],Res);
1.76 val ((pt,_),_) = get_calc 1;
1.77 - if "2 + -1 + x = 2" = UnparseC.term (fst (get_obj g_result pt [1,6])) then()
1.78 + if "2 + - 1 + x = 2" = UnparseC.term (fst (get_obj g_result pt [1,6])) then()
1.79 else error "inform.sml: diff.behav.appendFormula: on Frm + equ 1";
1.80
1.81 fetchProposedTactic 1; (*takes Iterator 1 _1_*)
1.82 @@ -179,7 +179,7 @@
1.83 Iterator 1; moveActiveRoot 1;
1.84 autoCalculate 1 CompleteCalcHead;
1.85 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
1.86 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
1.87 + autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + - 1 * 2 = 0*);
1.88
1.89 appendFormula 1 "x = 2" (*|> Future.join*);
1.90 val ((pt,p),_) = get_calc 1;
1.91 @@ -212,13 +212,13 @@
1.92 Iterator 1; moveActiveRoot 1;
1.93 autoCalculate 1 CompleteCalcHead;
1.94 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
1.95 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
1.96 + autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + - 1 * 2 = 0*);
1.97
1.98 appendFormula 1 "x = 1" (*|> Future.join*);
1.99 val ((pt,p),_) = get_calc 1;
1.100 val str = pr_ctree pr_short pt;
1.101 writeln str;
1.102 - if str = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n3. ----- pblobj -----\n3.1. -1 + x = 0\n3.2. x = 0 + -1 * -1\n3.2.1. x = 0 + -1 * -1\n3.2.2. x = 0 + 1\n" andalso p = ([3,2], Res)
1.103 + if str = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + - 1 * 2 = 0\n3. ----- pblobj -----\n3.1. - 1 + x = 0\n3.2. x = 0 + - 1 * - 1\n3.2.1. x = 0 + - 1 * - 1\n3.2.2. x = 0 + 1\n" andalso p = ([3,2], Res)
1.104 then () (*finds 1 step too early: ([3,2], Res) "x = 1" also by script !!!*)
1.105 else error "inform.sml: diff.behav.appendFormula: Res + late d 1";
1.106
1.107 @@ -232,9 +232,9 @@
1.108 else error "inform.sml: diff.behav.appendFormula: Res + late d 3";
1.109 DEconstrCalcTree 1;
1.110
1.111 -"--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";
1.112 -"--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";
1.113 -"--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";
1.114 +"--------- appendFormula: on Res + late deriv [x = 3 + - 2]---///--";
1.115 +"--------- appendFormula: on Res + late deriv [x = 3 + - 2]---///--";
1.116 +"--------- appendFormula: on Res + late deriv [x = 3 + - 2]---///--";
1.117 reset_states ();
1.118 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1.119 ("Test", ["sqroot-test", "univariate", "equation", "test"],
1.120 @@ -242,16 +242,16 @@
1.121 Iterator 1; moveActiveRoot 1;
1.122 autoCalculate 1 CompleteCalcHead;
1.123 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
1.124 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
1.125 + autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + - 1 * 2 = 0*);
1.126 appendFormula 1 "[x = 3 + -2*1]" (*|> Future.join*);
1.127 val ((pt,p),_) = get_calc 1;
1.128 val str = pr_ctree pr_short pt;
1.129 writeln str;
1.130 - if str=". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n3. ----- pblobj -----\n3.1. -1 + x = 0\n3.2. x = 0 + -1 * -1\n4. [x = 1]\n4.1. [x = 1]\n4.2. [x = -2 + 3]\n4.3. [x = 3 + -2]\n" then ()
1.131 + if str=". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + - 1 * 2 = 0\n3. ----- pblobj -----\n3.1. - 1 + x = 0\n3.2. x = 0 + - 1 * - 1\n4. [x = 1]\n4.1. [x = 1]\n4.2. [x = - 2 + 3]\n4.3. [x = 3 + - 2]\n" then ()
1.132 else error "inform.sml: diff.behav.appendFormula: Res + latEE 1";
1.133 autoCalculate 1 CompleteCalc;
1.134 val ((pt,p),_) = get_calc 1;
1.135 - if "[x = 3 + -2 * 1]" = UnparseC.term (fst (get_obj g_result pt [])) then ()
1.136 + if "[x = 3 + - 2 * 1]" = UnparseC.term (fst (get_obj g_result pt [])) then ()
1.137 (* ~~~~~~~~~~ simplify as last step in any script ?!*)
1.138 else error "inform.sml: diff.behav.appendFormula: Res + latEE 2";
1.139 DEconstrCalcTree 1;
1.140 @@ -266,8 +266,8 @@
1.141 Iterator 1; moveActiveRoot 1;
1.142 autoCalculate 1 CompleteCalcHead;
1.143 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
1.144 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
1.145 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*-1 + x*);
1.146 + autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + - 1 * 2 = 0*);
1.147 + autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*- 1 + x*);
1.148
1.149 replaceFormula 1 "-2 * 1 + (1 + x) = 0"; refFormula 1 (get_pos 1 1);
1.150 val ((pt,_),_) = get_calc 1;
1.151 @@ -276,10 +276,10 @@
1.152 (* before AK110725 this was
1.153 ". ----- pblobj -----\n
1.154 1. x + 1 = 2\n
1.155 -2. x + 1 + -1 * 2 = 0\n
1.156 -2.1. x + 1 + -1 * 2 = 0\n
1.157 -2.2. 1 + x + -1 * 2 = 0\n
1.158 -2.3. 1 + (x + -1 * 2) = 0\n
1.159 +2. x + 1 + - 1 * 2 = 0\n
1.160 +2.1. x + 1 + - 1 * 2 = 0\n
1.161 +2.2. 1 + x + - 1 * 2 = 0\n
1.162 +2.3. 1 + (x + - 1 * 2) = 0\n
1.163 2.4. 1 + (x + -2) = 0\n
1.164 2.5. 1 + (x + -2 * 1) = 0\n
1.165 2.6. 1 + x + -2 * 1 = 0\n";
1.166 @@ -287,13 +287,13 @@
1.167 if str =
1.168 ". ----- pblobj -----\n"^
1.169 "1. x + 1 = 2\n"^
1.170 -"2. x + 1 + -1 * 2 = 0\n"^
1.171 -"2.1. x + 1 + -1 * 2 = 0\n"^
1.172 -"2.2. 1 + x + -1 * 2 = 0\n"^
1.173 -"2.3. 1 + (x + -1 * 2) = 0\n"^
1.174 -"2.4. 1 + (x + -2) = 0\n"^
1.175 -"2.5. 1 + (x + -2 * 1) = 0\n"^
1.176 -"2.6. 1 + x + -2 * 1 = 0\n" then()
1.177 +"2. x + 1 + - 1 * 2 = 0\n"^
1.178 +"2.1. x + 1 + - 1 * 2 = 0\n"^
1.179 +"2.2. 1 + x + - 1 * 2 = 0\n"^
1.180 +"2.3. 1 + (x + - 1 * 2) = 0\n"^
1.181 +"2.4. 1 + (x + - 2) = 0\n"^
1.182 +"2.5. 1 + (x + - 2 * 1) = 0\n"^
1.183 +"2.6. 1 + x + - 2 * 1 = 0\n" then()
1.184 else error "inform.sml: diff.behav.replaceFormula: on Res += 1";
1.185
1.186 autoCalculate 1 CompleteCalc;
1.187 @@ -312,13 +312,13 @@
1.188 Iterator 1; moveActiveRoot 1;
1.189 autoCalculate 1 CompleteCalcHead;
1.190 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
1.191 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
1.192 + autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + - 1 * 2 = 0*);
1.193
1.194 replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1);
1.195 val ((pt,_),_) = get_calc 1;
1.196 val str = pr_ctree pr_short pt;
1.197 writeln str;
1.198 - if str= ". ----- pblobj -----\n1. x + 1 = 2\n1.1. x + 1 = 2\n1.2. 1 + x = 2\n1.3. 1 + x = -2 + 4\n1.4. x + 1 = -2 + 4\n" then ()
1.199 + if str= ". ----- pblobj -----\n1. x + 1 = 2\n1.1. x + 1 = 2\n1.2. 1 + x = 2\n1.3. 1 + x = - 2 + 4\n1.4. x + 1 = - 2 + 4\n" then ()
1.200 else error "inform.sml: diff.behav.replaceFormula: on Res 1 + = 1";
1.201 autoCalculate 1 CompleteCalc;
1.202 val ((pt,pos as (p,_)),_) = get_calc 1;
1.203 @@ -341,7 +341,7 @@
1.204 val ((pt,_),_) = get_calc 1;
1.205 val str = pr_ctree pr_short pt;
1.206 writeln str;
1.207 - if str= ". ----- pblobj -----\n1. x + 1 = 2\n1.1. x + 1 = 2\n1.2. 1 + x = 2\n1.3. 1 + x = -2 + 4\n1.4. x + 1 = -2 + 4\n" then ()
1.208 + if str= ". ----- pblobj -----\n1. x + 1 = 2\n1.1. x + 1 = 2\n1.2. 1 + x = 2\n1.3. 1 + x = - 2 + 4\n1.4. x + 1 = - 2 + 4\n" then ()
1.209 else error "inform.sml: diff.behav.replaceFormula: on Frm 1 + = 1";
1.210 autoCalculate 1 CompleteCalc;
1.211 val ((pt,pos as (p,_)),_) = get_calc 1;
1.212 @@ -456,7 +456,7 @@
1.213 Iterator 1; moveActiveRoot 1;
1.214 autoCalculate 1 CompleteCalcHead;
1.215 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
1.216 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
1.217 + autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + - 1 * 2 = 0*);
1.218
1.219 appendFormula 1 " x - "; (*<ERROR> syntax error in ' x - ' </ERROR>*)
1.220 val ((pt,_),_) = get_calc 1;
1.221 @@ -512,7 +512,7 @@
1.222 Iterator 1; moveActiveRoot 1;
1.223 autoCalculate 1 CompleteCalcHead;
1.224
1.225 -"--- (-1) give a preview on the calculation without any input";
1.226 +"--- (- 1) give a preview on the calculation without any input";
1.227 (*
1.228 autoCalculate 1 CompleteCalc;
1.229 val ((pt, p), _) = get_calc 1;
1.230 @@ -1277,13 +1277,13 @@
1.231 "--------- fun concat_deriv --------------------------------------";
1.232 (*
1.233 val ({rew_ord, erls, rules,...}, fo, ifo) =
1.234 - (Rule_Set.rep Test_simplify, TermC.str2term "x+1+ -1*2=0", TermC.str2term "-2*1+(x+1)=0");
1.235 + (Rule_Set.rep Test_simplify, TermC.str2term "x+1+ - 1*2=0", TermC.str2term "-2*1+(x+1)=0");
1.236 (tracing o Derive.trtas2str) fod';
1.237 > ["
1.238 -(x + 1 + -1 * 2 = 0, Thm ("radd_commute", "?m + ?n = ?n + ?m"), (-1 * 2 + (x + 1) = 0, []))", "
1.239 -(-1 * 2 + (x + 1) = 0, Thm ("radd_commute", "?m + ?n = ?n + ?m"), (-1 * 2 + (1 + x) = 0, []))", "
1.240 -(-1 * 2 + (1 + x) = 0, Thm ("radd_left_commute", "?x + (?y + ?z) = ?y + (?x + ?z)"), (1 + (-1 * 2 + x) = 0, []))", "
1.241 -(1 + (-1 * 2 + x) = 0, Thm ("#mult_Float ((~1,0), (0,0)) __ ((2,0), (0,0))", "-1 * 2 = -2"), (1 + (-2 + x) = 0, []))"]
1.242 +(x + 1 + - 1 * 2 = 0, Thm ("radd_commute", "?m + ?n = ?n + ?m"), (- 1 * 2 + (x + 1) = 0, []))", "
1.243 +(- 1 * 2 + (x + 1) = 0, Thm ("radd_commute", "?m + ?n = ?n + ?m"), (- 1 * 2 + (1 + x) = 0, []))", "
1.244 +(- 1 * 2 + (1 + x) = 0, Thm ("radd_left_commute", "?x + (?y + ?z) = ?y + (?x + ?z)"), (1 + (- 1 * 2 + x) = 0, []))", "
1.245 +(1 + (- 1 * 2 + x) = 0, Thm ("#mult_Float ((~1,0), (0,0)) __ ((2,0), (0,0))", "- 1 * 2 = -2"), (1 + (-2 + x) = 0, []))"]
1.246 val it = () : unit
1.247 (tracing o Derive.trtas2str) (map Derive.rev_deriv' rifod');
1.248 > ["
1.249 @@ -1327,7 +1327,7 @@
1.250 ------------------------------------------------------------------------------
1.251 1. "x / (x \<up> 2 - 6 * x + 9) - 1 / (x \<up> 2 - 3 * x) = 1 / x"
1.252 ...
1.253 -4. "(3 + (-1 * x + x \<up> 2)) * x = 1 * (9 * x + (x \<up> 3 + -6 * x \<up> 2))"
1.254 +4. "(3 + (- 1 * x + x \<up> 2)) * x = 1 * (9 * x + (x \<up> 3 + -6 * x \<up> 2))"
1.255 Subproblem["normalise", "polynomial", "univariate"..
1.256 ...
1.257 4.4. "-6 * x + 5 * x \<up> 2 = 0", Subproblem["bdv_only", "degree_2", "poly"..