1.1 --- a/TODO.md Wed Aug 03 17:18:47 2022 +0200
1.2 +++ b/TODO.md Wed Aug 03 18:06:02 2022 +0200
1.3 @@ -79,12 +79,6 @@
1.4 (*2*)val _ = @{print tracing}{a = "hd_ord (f, g) = ", z = hd_ord (f, g)}(**)
1.5
1.6
1.7 -* WN: eliminate global flags like "trace_on", replace Unsynchronized.ref by
1.8 -
1.9 -ML \<open>
1.10 - val rewrite_trace = Attrib.setup_config_bool \<^binding>\<open>rewrite_trace\<close> (K false);
1.11 -\<close>
1.12 -
1.13 * WN: Calculate.thy: add structure Calculate
1.14 * WN: cleanup method-def.sml, problem-def.sml, "eval-def.sml", "rewrite-order.sml"
1.15 * WN: MethodC.from_store throws exn 'get_pbt not found: ' ... confusing !! take 'ketype' as an argument
2.1 --- a/src/Tools/isac/BaseDefinitions/rewrite-order.sml Wed Aug 03 17:18:47 2022 +0200
2.2 +++ b/src/Tools/isac/BaseDefinitions/rewrite-order.sml Wed Aug 03 18:06:02 2022 +0200
2.3 @@ -32,16 +32,6 @@
2.4 fun to_string (rew_ord', _) = "(" ^ rew_ord' ^ ", _: fn)"
2.5
2.6 type rew_ord' = Rule_Def.rew_ord'
2.7 -(* rewrite orders, also stored in 'type met' and type 'and rls'
2.8 - The association list is required for 'rewrite.."rew_ord"..' *)
2.9 -val rew_ord' = Unsynchronized.ref
2.10 - ([("e_rew_ord", e_rew_ord), ("dummy_ord", dummy_ord)]
2.11 - : (rew_ord' * (* the key for the association list *)
2.12 - (subst (* the bound variables - they get high order*)
2.13 - -> (term * term) (* (t1, t2) to be compared *)
2.14 - -> bool)) (* if t1 <= t2 then true else false *)
2.15 - list); (* association list *)
2.16 -
2.17 fun equal ((id1, _), (id2, _)) = id1 = id2
2.18
2.19 end
3.1 --- a/src/Tools/isac/Build_Isac.thy Wed Aug 03 17:18:47 2022 +0200
3.2 +++ b/src/Tools/isac/Build_Isac.thy Wed Aug 03 18:06:02 2022 +0200
3.3 @@ -200,12 +200,7 @@
3.4 \<close>
3.5 subsection \<open>(0) Survey on remaining Unsynchronized.ref\<close>
3.6 text \<open>
3.7 - REPLACE BY Know_Store... (has been overlooked)
3.8 - calcelems.sml:val rew_ord' = Unsynchronized.ref ...
3.9 - KEEP FOR DEMOS
3.10 - Knowledge/GCD_Poly_ML.thy: val trace_div = Unsynchronized.ref true;
3.11 - Knowledge/GCD_Poly_ML.thy: val trace_div_invariant = Unsynchronized.ref false;
3.12 - Knowledge/GCD_Poly_ML.thy: val trace_Euclid = Unsynchronized.ref true;
3.13 + DONE
3.14 \<close>
3.15 subsection \<open>(1) Exploit parallelism for concurrent session management\<close>
3.16 subsection \<open>(2) Make Isac’s programming language usable\<close>
4.1 --- a/src/Tools/isac/Knowledge/GCD_Poly_ML.thy Wed Aug 03 17:18:47 2022 +0200
4.2 +++ b/src/Tools/isac/Knowledge/GCD_Poly_ML.thy Wed Aug 03 18:06:02 2022 +0200
4.3 @@ -964,8 +964,11 @@
4.4 replicate 3 0 = [0, 0, 0];
4.5 replicate 0 0 = [];
4.6
4.7 - val trace_div = Unsynchronized.ref true;
4.8 - val trace_div_invariant = Unsynchronized.ref false; (*.. true expects !trace_div = false *)
4.9 + val trace_div = Attrib.setup_config_bool \<^binding>\<open>trace_div\<close> (K true);
4.10 + val trace_div_invariant = Attrib.setup_config_bool \<^binding>\<open>trace_div_invariant\<close>
4.11 + (K false); (*.. true expects !trace_div = false *)
4.12 + val trace_Euclid = Attrib.setup_config_bool \<^binding>\<open>trace_Euclid\<close> (K true);
4.13 +
4.14 fun div_invariant2 p1 p2 n ns zeros q quot remd =
4.15 (@{make_string} p1 ^ " * " ^ @{make_string} (n * ns) ^ " = " ^
4.16 @{make_string} (mult_to_deg (deg_up p1 - deg_up p2)
4.17 @@ -973,7 +976,7 @@
4.18 " ** " ^ @{make_string} p2 ^ " ++ " ^
4.19 @{make_string} ((rev o (mult_to_deg (deg_up p1)) o rev) remd))
4.20 fun writeln_trace p1 p1' p2 quot n q (zeros:int) remd (ns: int) =
4.21 - (if (! trace_div) then
4.22 + (if Config.get @{context} trace_div then
4.23 ( writeln (" div " ^ @{make_string} p1' ^ " * " ^ @{make_string} n);
4.24 writeln " div ~~~~~~~~~~~~~~~~~~~~~~~~~~~";
4.25 writeln (" div " ^ @{make_string} (p1' %* n));
4.26 @@ -995,7 +998,7 @@
4.27 ((mult_to_deg (deg_up p1 - deg_up p2)
4.28 ((replicate zeros 0) @ [q] @ (quot %* n)) %*% p2 %+% remd))
4.29 then
4.30 - if (! trace_div_invariant)
4.31 + if Config.get @{context} trace_div_invariant
4.32 then writeln (" div " ^ div_invariant2 p1 p2 n ns (replicate zeros 0) q quot remd)
4.33 else ()
4.34 else raise ERROR ("invariant 2 does not hold: " ^ div_invariant2 p1 p2 n ns (replicate zeros 0) q quot remd)
4.35 @@ -1029,7 +1032,7 @@
4.36 fun p1 %*/% p2 =
4.37 let
4.38 val (n, q, r) = div_int_up p1 p1 p2 [] 1
4.39 - val _ = if (! trace_div) then
4.40 + val _ = if Config.get @{context} trace_div then
4.41 (writeln " div .....................................................................";
4.42 writeln (" div " ^ @{make_string} n ^ " * " ^ @{make_string} p1 ^ " = " ^
4.43 @{make_string} q ^ " ** " ^ @{make_string} p2 ^ " ++ " ^ @{make_string} r);
4.44 @@ -1038,9 +1041,9 @@
4.45 in (n, q, r) end;
4.46 \<close>
4.47 text \<open>Here is the check of the algorithm with the values from above: [[1]]\<close>
4.48 +declare [[trace_div = true]]
4.49 +declare [[trace_div_invariant = false]]
4.50 ML \<open>
4.51 - trace_div := true;
4.52 - trace_div_invariant := false;
4.53 val p1 = [2, 2, 2, 2, 2];
4.54 val p2 = [1, 2, 3];
4.55 val (n (* = 27*),
4.56 @@ -1072,9 +1075,8 @@
4.57 division of integers in the Euclidean Algorithm:
4.58 \<close>
4.59 ML \<open>
4.60 - val trace_Euclid = Unsynchronized.ref true;
4.61 fun writeln_trace_Euclid (a: int list) (b: int list) (n: int) (q: int list) (r: int list) =
4.62 - if (! trace_Euclid) then
4.63 + if Config.get @{context} trace_Euclid then
4.64 writeln ("Euclid " ^ @{make_string} a ^ " * " ^ @{make_string} n ^
4.65 " == " ^ @{make_string} q ^
4.66 " ** " ^ @{make_string} b ^ " ++ " ^ @{make_string} r)
4.67 @@ -1088,11 +1090,11 @@
4.68 val _ = writeln_trace_Euclid a b n q r
4.69 in EUCLID_naive_up b r : unipoly end;
4.70 \<close>
4.71 +declare [[trace_div = false]]
4.72 +declare [[trace_div_invariant = false]]
4.73 +declare [[trace_Euclid = true]]
4.74 ML \<open>
4.75 (*The example used in the inital mail to Tobias Nipkow made univariate: y -> 1*)
4.76 - trace_div := false;
4.77 - trace_div_invariant := false;
4.78 - trace_Euclid := true;
4.79 "--------------------------------";
4.80 val a = [0,~1,1]: unipoly; (* -x + x^2 = x *(-1 + x) *)
4.81 val b = [~1,0,1]: unipoly; (* -1 + x^2 = (1+x)*(-1 + x) *)
4.82 @@ -1139,10 +1141,10 @@
4.83 Euclids Algorithm in modern algebraic notation explains itself if presented
4.84 this way:
4.85 \<close>
4.86 +declare [[trace_div = false]]
4.87 +declare [[trace_div_invariant = false]]
4.88 +declare [[trace_Euclid = true]]
4.89 ML \<open>
4.90 - trace_div := false;
4.91 - trace_div_invariant := false;
4.92 - trace_Euclid := true;
4.93 "--------------------------------";
4.94 val a = [~1,0,0,1]: unipoly; (* -1 + x^3 = (1+x+x^2)*(-1 + x) *)
4.95 val b = [0,~1,1]: unipoly; (* -x + x^2 = x *(-1 + x) *)
4.96 @@ -1153,8 +1155,8 @@
4.97 Euclid [0, ~1, 1] * 1 == [0, 1] ** [~1, 1] ++ []
4.98 *)
4.99 \<close>
4.100 +declare [[trace_Euclid = true]]
4.101 ML \<open>
4.102 - trace_Euclid := true;
4.103 (* from [1].p.94 *)
4.104 "--------------------------------";
4.105 val a = [~18, ~15, ~20, 12, 20, ~13, 2]: unipoly;
4.106 @@ -1194,9 +1196,9 @@
4.107
4.108 Case (1) again calls for the fixpoint:
4.109 \<close>
4.110 +declare [[trace_div = false]]
4.111 +declare [[trace_div_invariant = true]]
4.112 ML \<open>
4.113 - trace_div := false;
4.114 - trace_div_invariant := true;
4.115 val p1 = [2, 2, 2, 2, 2];
4.116 val p2 = [1, 2, 3];
4.117 val (n (* = 27*),
4.118 @@ -1216,9 +1218,9 @@
4.119 This representation, however, is inappropriate for reproduction by hand.
4.120 Dividing polynomials by hand is taught in this format:
4.121 \<close>
4.122 +declare [[trace_div = true]]
4.123 +declare [[trace_div_invariant = false]]
4.124 ML \<open>
4.125 - trace_div := true;
4.126 - trace_div_invariant := false;
4.127 val p1 = [2, 2, 2, 2, 2];
4.128 val p2 = [1, 2, 3];
4.129 val (n (* = 27*),
4.130 @@ -1254,8 +1256,8 @@
4.131 Thus the quotient needs to be multiplied subsequently as well.
4.132 The algorithm also has to handle cases, where zeros occur in the quotient:
4.133 \<close>
4.134 +declare [[trace_div = true]]
4.135 ML \<open>
4.136 - trace_div := true;
4.137 val p1 = [3,2,2,2,1,1,1,1];
4.138 val p2 = [1,1,1,1];
4.139 val (n (* = 1*),
4.140 @@ -1362,9 +1364,9 @@
4.141 PSEUDO-division is "%*/%";
4.142 we set switches to create output as found in the extended abstract:
4.143 \<close>
4.144 +declare [[trace_div = false]]
4.145 +declare [[trace_div_invariant = true]]
4.146 ML \<open>
4.147 - trace_div_invariant := true;
4.148 - trace_div := false;
4.149 \<close> ML \<open>
4.150 [1, 2, 3, 4, 5, 6] %*/% [7, 8, 9]
4.151 \<close>
4.152 @@ -1372,10 +1374,9 @@
4.153 We need a notepad for interactive trials!
4.154 And this gives the invariant of the GCD:
4.155 \<close>
4.156 +declare [[trace_div = true]]
4.157 +declare [[trace_div_invariant = false]]
4.158 ML \<open>
4.159 - trace_Euclid := true;
4.160 - trace_div_invariant := false;
4.161 - trace_div := false;
4.162 EUCLID_naive_up [~18, ~15, ~20, 12, 20, ~13, 2] [8, 28, 22, ~11, ~14, 1, 2]
4.163 \<close>
4.164 thm gcd_add_mult
4.165 @@ -1384,9 +1385,9 @@
4.166 text \<open>
4.167 We take smaller polynomials for DIV;
4.168 \<close>
4.169 +declare [[trace_div = true]]
4.170 +declare [[trace_div_invariant = false]]
4.171 ML \<open>
4.172 - trace_div := true;
4.173 - trace_div_invariant := false;
4.174 [4, 3, 2, 1] %*/% [2, 1]
4.175 \<close>
4.176 text \<open>
5.1 --- a/src/Tools/isac/MathEngBasic/rewrite.sml Wed Aug 03 17:18:47 2022 +0200
5.2 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml Wed Aug 03 18:06:02 2022 +0200
5.3 @@ -50,7 +50,7 @@
5.4
5.5 exception NO_REWRITE;
5.6
5.7 -(* depth of recursion in traces of the rewriter, if trace_on:=true *)
5.8 +(* depth of recursion in traces of the rewriter, if trace_on = true *)
5.9 val rewrite_trace_depth = Attrib.setup_config_int \<^binding>\<open>rewrite_trace_depth\<close> (K 99999);
5.10
5.11 fun trace ctxt i str =
6.1 --- a/test/Tools/isac/Knowledge/gcd_poly_ml.sml Wed Aug 03 17:18:47 2022 +0200
6.2 +++ b/test/Tools/isac/Knowledge/gcd_poly_ml.sml Wed Aug 03 18:06:02 2022 +0200
6.3 @@ -1129,9 +1129,10 @@
6.4 "----------- last step in EUCLID ------------------------";
6.5 "----------- last step in EUCLID ------------------------";
6.6 "----------- last step in EUCLID ------------------------";
6.7 -trace_div := false;
6.8 -trace_div_invariant := false;
6.9 -trace_Euclid := false;
6.10 +(* declare [[trace_div = false]] *)
6.11 +(* declare [[trace_div_invariant = false]] *)
6.12 +(* declare [[trace_Euclid = false]] *)
6.13 +
6.14 val a = [~18, ~15, ~20, 12, 20, ~13, 2];
6.15 val b = [8, 28, 22, ~11, ~14, 1, 2];
6.16 "~1~~~~ fun EUCLID_naive_up, args:"; val (a, b) = (a, b);