1.1 --- a/TODO.md Sat Aug 06 10:45:24 2022 +0200
1.2 +++ b/TODO.md Sat Aug 06 15:02:55 2022 +0200
1.3 @@ -33,12 +33,6 @@
1.4 (*1*)val _ = tracing ("hd_ord (f, g) = " ^ ((pr_ord o hd_ord) (f, g)) );
1.5 (*2*)val _ = @{print tracing}{a = "hd_ord (f, g) = ", z = hd_ord (f, g)}(**)
1.6
1.7 -* KEStore_Elems: Should we eliminate union_overwrite and use standard namespace merge?
1.8 - (Exception: rlss with its special cross-theory merge.)
1.9 - ? how adapt the different signatures ?
1.10 - union_overwrite: ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list
1.11 - merge : ('a * 'a -> bool) -> 'a list * 'a list -> 'a list
1.12 -
1.13
1.14 ***** for the few items below WN asks MW for help
1.15
2.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy Sat Aug 06 10:45:24 2022 +0200
2.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy Sat Aug 06 15:02:55 2022 +0200
2.3 @@ -91,8 +91,6 @@
2.4
2.5 structure KEStore_Elems(**): KESTORE_ELEMS(**) =
2.6 struct
2.7 - fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1;
2.8 -
2.9 structure Data = Theory_Data (
2.10 type T = (string * (LibraryC.subst -> term * term -> bool)) list;
2.11 val empty = [];
2.12 @@ -100,7 +98,7 @@
2.13 val merge = merge Rewrite_Ord.equal;
2.14 );
2.15 fun get_rew_ord thy = Data.get thy
2.16 - fun add_rew_ord rlss = Data.map (union_overwrite Rewrite_Ord.equal rlss)
2.17 + fun add_rew_ord rlss = Data.map (curry (Library.merge Rewrite_Ord.equal) rlss)
2.18
2.19 structure Data = Theory_Data (
2.20 type T = (Rule_Set.id * (ThyC.id * Rule_Set.T)) list;
2.21 @@ -109,7 +107,7 @@
2.22 val merge = Rule_Set.to_kestore;
2.23 );
2.24 fun get_rlss thy = Data.get thy
2.25 - fun add_rlss rlss = Data.map (union_overwrite Rule_Set.equal rlss)
2.26 + fun add_rlss rlss = Data.map (curry (Library.merge Rule_Set.equal) rlss)
2.27
2.28 structure Data = Theory_Data (
2.29 type T = (Eval_Def.prog_calcID * (Eval_Def.calID * Eval_Def.eval_fn)) list;
2.30 @@ -118,7 +116,7 @@
2.31 val merge = merge Eval_Def.calc_eq;
2.32 );
2.33 fun get_calcs thy = Data.get thy
2.34 - fun add_calcs calcs = Data.map (union_overwrite Eval_Def.calc_eq calcs)
2.35 + fun add_calcs calcs = Data.map (curry (Library.merge Eval_Def.calc_eq) calcs)
2.36
2.37 structure Data = Theory_Data (
2.38 type T = (term * (References_Def.T * (term list -> (term * term list) list))) list;
2.39 @@ -127,7 +125,7 @@
2.40 val merge = merge CAS_Def.equal;
2.41 );
2.42 fun get_cas thy = Data.get thy
2.43 - fun add_cas cas = Data.map (union_overwrite CAS_Def.equal cas)
2.44 + fun add_cas cas = Data.map (curry (Library.merge CAS_Def.equal) cas)
2.45
2.46 structure Data = Theory_Data (
2.47 type T = Probl_Def.store;
2.48 @@ -358,6 +356,23 @@
2.49 \<close>
2.50 ML \<open>
2.51 \<close> ML \<open>
2.52 + fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1;
2.53 +\<close> ML \<open>
2.54 +union_overwrite: ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list;
2.55 +merge : ('a * 'a -> bool) -> 'a list * 'a list -> 'a list
2.56 +\<close> ML \<open>
2.57 +val eq = op=;
2.58 +val l1 = [1,2,3,4,5];
2.59 +val l2 = [4,5,6,7,8];
2.60 +\<close> ML \<open>
2.61 +union_overwrite eq l1 l2 = [8, 7, 6, 1, 2, 3, 4, 5];
2.62 +Library.merge eq (l1, l2) = [6, 7, 8, 1, 2, 3, 4, 5]
2.63 +\<close> ML \<open>
2.64 +\<close> ML \<open>
2.65 +Library.merge eq (*: _a list * _a list -> _a list*);
2.66 +curry (Library.merge eq)(*: _a list -> _a list -> _a list*)
2.67 +\<close> ML \<open>
2.68 +\<close> ML \<open>
2.69 \<close> ML \<open>
2.70 \<close>
2.71 end
3.1 --- a/test/Tools/isac/ADDTESTS/accumulate-val/lucas_interpreter.sml Sat Aug 06 10:45:24 2022 +0200
3.2 +++ b/test/Tools/isac/ADDTESTS/accumulate-val/lucas_interpreter.sml Sat Aug 06 15:02:55 2022 +0200
3.3 @@ -16,8 +16,6 @@
3.4
3.5 structure Test_KEStore_Elems: KESTORE_ELEMS =
3.6 struct
3.7 - fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1;
3.8 -
3.9 fun rls_eq ((id1, (thyID1, _)), (id2, (thyID2, _))) = id1 = id2 (*andalso thyID1 = thyID2*)
3.10 structure Data = Theory_Data (
3.11 type T = (Rule_Set.id * (ThyC.id * Rule_Set.T)) list;
3.12 @@ -26,7 +24,7 @@
3.13 val merge = merge rls_eq;
3.14 );
3.15 fun get_rlss thy = Data.get thy
3.16 - fun add_rlss rlss = Data.map (union_overwrite rls_eq rlss)
3.17 + fun add_rlss rlss = Data.map (curry (Library.merge rls_eq) rlss)
3.18
3.19 val calc_eq = rls_eq
3.20 structure Data = Theory_Data (
3.21 @@ -36,7 +34,7 @@
3.22 val merge = merge calc_eq;
3.23 );
3.24 fun get_calcs thy = Data.get thy
3.25 - fun add_calcs calcs = Data.map (union_overwrite calc_eq calcs)
3.26 + fun add_calcs calcs = Data.map (curry (Library.merge calc_eq) calcs)
3.27
3.28 (*etc*)
3.29 end;
4.1 --- a/test/Tools/isac/BaseDefinitions/kestore.sml Sat Aug 06 10:45:24 2022 +0200
4.2 +++ b/test/Tools/isac/BaseDefinitions/kestore.sml Sat Aug 06 15:02:55 2022 +0200
4.3 @@ -33,7 +33,6 @@
4.4 "-------- fun Test_KEStore_Elems.add_rlss overwrites earlier data -----------------";
4.5 "-------- fun Test_KEStore_Elems.add_rlss overwrites earlier data -----------------";
4.6 "-------- fun Test_KEStore_Elems.add_rlss overwrites earlier data -----------------";
4.7 - fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1;
4.8 fun rls_eq ((id1, (thyID1, _)), (id2, (thyID2, _))) = id1 = id2 (*andalso thyID1 = thyID2*)
4.9
4.10 val data1 = [("test", ("theory-1", Rule_Set.Empty)),
4.11 @@ -43,7 +42,7 @@
4.12 [("test_rls", ("theory-2",
4.13 Rule_Set.append_rules "test_rls" Rule_Set.empty [Thm ("not_def", @{thm not_def})]))]
4.14 val data_3a = union rls_eq data1 data2
4.15 -val data_3b = union_overwrite rls_eq data1 data2
4.16 +val data_3b = Library.merge rls_eq (data1, data2)
4.17
4.18 val SOME (_, Rule_Set.Repeat {rules, ...}) = AList.lookup op = data_3a "test_rls";
4.19 case rules of
4.20 @@ -53,9 +52,9 @@
4.21 val SOME (_, Rule_Set.Repeat {rules, ...}) = AList.lookup op = data_3b "test_rls";
4.22 case rules of
4.23 [Thm ("refl", _), Thm ("subst", _)] => ()
4.24 -| _ => error "union_overwrite rls_eq changed: 2nd argument is NOT overwritten anymore"
4.25 +| _ => error "Library.merge rls_eq changed: 2nd argument is NOT overwritten anymore"
4.26
4.27 -(* add_rlss will take union_overwrite due to argument sequence *)
4.28 +(* add_rlss will take Library.merge due to argument sequence *)
4.29
4.30
4.31 "-------- ERROR assoc_calc: 'Prog_Expr.is_num' not found in theory Poly ------";
4.32 @@ -87,7 +86,7 @@
4.33 val calcs =
4.34 KEStore_Elems.get_calcs thy;
4.35
4.36 -(*+*)val ("is_polyrat_in", ("Poly.is_polyrat_in", _)) = nth 17 calcs; (* <<<<<------- is_atom <> is_num *)
4.37 +(*+*)val ("matches", ("Prog_Expr.matches", _)) = nth 17 calcs;
4.38 (*+*)map fst calcs = (*..WITH declare [[ML_print_depth = 999]]*)
4.39 ["Test.precond_rootmet", "contains_root", "Test.precond_rootpbl", "is_f_x", "primed", "is_normSqrtTerm_in", "is_rootTerm_in", "SQRT", "is_sqrtTerm_in", "is_ratequation_in", "is_rootRatAddTerm_in", "add_new_c",
4.40 "occur_exactly_in", "is_addUnordered", "is_polyexp", "is_poly_in", "is_polyrat_in", "POWER", "TIMES", "PLUS", "ident", "le", "is_atom", "occurs_in", "is_num", "matchsub", "Vars", "lhs", "rhs", "matches",
5.1 --- a/test/Tools/isac/Knowledge/poly-2.sml Sat Aug 06 10:45:24 2022 +0200
5.2 +++ b/test/Tools/isac/Knowledge/poly-2.sml Sat Aug 06 15:02:55 2022 +0200
5.3 @@ -116,7 +116,7 @@
5.4 val thm_isac = ThmC.sym_thm @{thm real_mult_minus1}; (* = "- ?z = - 1 * ?z" *)
5.5 val SOME t_isac = TermC.parseNEW @{context} "3 * a + - 1 * (2 * a):: real";
5.6
5.7 -val SOME (t', []) = rewrite_ @{theory} tless_true Rule_Set.empty true thm_isac t_isac;
5.8 +val SOME (t', []) = rewrite_ @{context} tless_true Rule_Set.empty true thm_isac t_isac;
5.9 if UnparseC.term t' = "3 * a + - 1 * 1 * (2 * a)" then ((*thm did NOT apply to Free ("- 1", _)*))
5.10 else error "thm - ?z = - 1 * ?z loops with new numerals";
5.11
5.12 @@ -124,48 +124,48 @@
5.13 "-------- rewrite_set_ has_degree_in Const ('Partial_Fractions', _) ----------------------------";
5.14 "-------- rewrite_set_ has_degree_in Const ('Partial_Fractions', _) ----------------------------";
5.15 "-------- rewrite_set_ has_degree_in Const ('Partial_Fractions', _) ----------------------------";
5.16 -val thy = @{theory Partial_Fractions}
5.17 -val expr = (Thm.term_of o the o (TermC.parse thy)) "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
5.18 +val thy = Proof_Context.init_global @{theory Partial_Fractions}
5.19 +val expr = TermC.parseNEW' thy "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
5.20 val SOME (Const (\<^const_name>\<open>True\<close>, _), []) = rewrite_set_ thy false PolyEq_prls expr;
5.21
5.22 -val expr = (Thm.term_of o the o (TermC.parse thy)) "((-8 - 2*AA + AA \<up> 2) has_degree_in AA) = 2";
5.23 +val expr = TermC.parseNEW' thy "((-8 - 2*AA + AA \<up> 2) has_degree_in AA) = 2";
5.24 val SOME (Const (\<^const_name>\<open>True\<close>, _), []) = rewrite_set_ thy false PolyEq_prls expr;
5.25
5.26 "-------- eval_ for is_expanded_in, is_poly_in, has_degree_in ----------------------------------";
5.27 "-------- eval_ for is_expanded_in, is_poly_in, has_degree_in ----------------------------------";
5.28 "-------- eval_ for is_expanded_in, is_poly_in, has_degree_in ----------------------------------";
5.29 -val t = (Thm.term_of o the o (TermC.parse thy)) "(-8 - 2*x + x \<up> 2) is_expanded_in x";
5.30 +val t = TermC.parseNEW' thy "(-8 - 2*x + x \<up> 2) is_expanded_in x";
5.31 val SOME (id, t') = eval_is_expanded_in 0 0 t 0;
5.32 if UnparseC.term t' = "- 8 - 2 * x + x \<up> 2 is_expanded_in x = True"
5.33 andalso id = "- 8 - 2 * x + x \<up> 2 is_expanded_in x = True"
5.34 then () else error "eval_is_expanded_in x ..changed";
5.35
5.36 -val thy = @{theory Partial_Fractions}
5.37 -val t = (Thm.term_of o the o (TermC.parse thy)) "(-8 - 2*AA + AA \<up> 2) is_expanded_in AA";
5.38 +val thy = Proof_Context.init_global @{theory Partial_Fractions}
5.39 +val t = TermC.parseNEW' thy "(-8 - 2*AA + AA \<up> 2) is_expanded_in AA";
5.40 val SOME (id, t') = eval_is_expanded_in 0 0 t 0;
5.41 if UnparseC.term t' = "- 8 - 2 * AA + AA \<up> 2 is_expanded_in AA = True"
5.42 andalso id = "- 8 - 2 * AA + AA \<up> 2 is_expanded_in AA = True"
5.43 then () else error "eval_is_expanded_in AA ..changed";
5.44
5.45
5.46 -val t = (Thm.term_of o the o (TermC.parse thy)) "(8 + 2*x + x \<up> 2) is_poly_in x";
5.47 +val t = TermC.parseNEW' thy "(8 + 2*x + x \<up> 2) is_poly_in x";
5.48 val SOME (id, t') = eval_is_poly_in 0 0 t 0;
5.49 if UnparseC.term t' = "8 + 2 * x + x \<up> 2 is_poly_in x = True"
5.50 andalso id = "8 + 2 * x + x \<up> 2 is_poly_in x = True"
5.51 then () else error "is_poly_in x ..changed";
5.52
5.53 -val t = (Thm.term_of o the o (TermC.parse thy)) "(8 + 2*AA + AA \<up> 2) is_poly_in AA";
5.54 +val t = TermC.parseNEW' thy "(8 + 2*AA + AA \<up> 2) is_poly_in AA";
5.55 val SOME (id, t') = eval_is_poly_in 0 0 t 0;
5.56 if UnparseC.term t' = "8 + 2 * AA + AA \<up> 2 is_poly_in AA = True"
5.57 andalso id = "8 + 2 * AA + AA \<up> 2 is_poly_in AA = True"
5.58 then () else error "is_poly_in AA ..changed";
5.59
5.60
5.61 -val thy = @{theory Partial_Fractions}
5.62 -val expr = (Thm.term_of o the o (TermC.parse thy)) "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
5.63 +val thy = Proof_Context.init_global @{theory Partial_Fractions}
5.64 +val expr = TermC.parseNEW' thy "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
5.65 val SOME (Const (\<^const_name>\<open>True\<close>, _), []) = rewrite_set_ thy false PolyEq_prls expr;
5.66
5.67 -val expr = (Thm.term_of o the o (TermC.parse thy)) "((-8 - 2*AA + AA \<up> 2) has_degree_in AA) = 2";
5.68 +val expr = TermC.parseNEW' thy "((-8 - 2*AA + AA \<up> 2) has_degree_in AA) = 2";
5.69 val SOME (Const (\<^const_name>\<open>True\<close>, _), []) = rewrite_set_ thy false PolyEq_prls expr;
5.70
5.71 "-------- investigate (new 2002) uniary minus --------------------------------------------------";
5.72 @@ -191,7 +191,7 @@
5.73 | _ => error "internal representation of \"0 - ?x = - ?x\" changed";
5.74
5.75
5.76 -val t = (Thm.term_of o the o (TermC.parse thy)) "- 1";
5.77 +val t = TermC.parseNEW' thy "- 1";
5.78 TermC.atomty t;
5.79 (*
5.80 ***
5.81 @@ -205,7 +205,7 @@
5.82 "======= these external values all have the same internal representation";
5.83 (* "1-x" causes syntyx error --- binary minus detected by blank inbetween !!!*)
5.84 (*----------------------------------- vvvvv -------------------------------------------*)
5.85 -val t = (Thm.term_of o the o (TermC.parse thy)) "-x";
5.86 +val t = TermC.parseNEW' thy "-x";
5.87 TermC.atomty t;
5.88 (**** -------------
5.89 *** Free ( -x, real)*)
5.90 @@ -213,7 +213,7 @@
5.91 Const (\<^const_name>\<open>uminus\<close>, _) $ Free ("x", _) => ()
5.92 | _ => error "internal representation of \"-x\" changed";
5.93 (*----------------------------------- vvvvv -------------------------------------------*)
5.94 -val t = (Thm.term_of o the o (TermC.parse thy)) "- x";
5.95 +val t = TermC.parseNEW' thy "- x";
5.96 TermC.atomty t;
5.97 (**** -------------
5.98 *** Free ( -x, real) !!!!!!!!!!!!!!!!!!!!!!!! is the same !!!*)
5.99 @@ -221,7 +221,7 @@
5.100 Const (\<^const_name>\<open>uminus\<close>, _) $ Free ("x", _) => ()
5.101 | _ => error "internal representation of \"- x\" changed";
5.102 (*----------------------------------- vvvvvv ------------------------------------------*)
5.103 -val t = (Thm.term_of o the o (TermC.parse thy)) "-(x)";
5.104 +val t = TermC.parseNEW' thy "-(x)";
5.105 TermC.atomty t;
5.106 (**** -------------
5.107 *** Free ( -x, real)*)
5.108 @@ -257,10 +257,10 @@
5.109 *)
5.110 val t = TermC.str2term "(1 + 2 * x \<up> 4 + - 4 * x \<up> 4 + x \<up> 8) is_addUnordered";
5.111
5.112 - eval_is_addUnordered "xxx" "yyy" t @{theory};
5.113 + eval_is_addUnordered "xxx" "yyy" t @{context};
5.114 "~~~~~ fun eval_is_addUnordered , args:"; val ((thmid:string), _,
5.115 (t as (Const (\<^const_name>\<open>is_addUnordered\<close>, _) $ arg)), thy) =
5.116 - ("xxx", "yyy", t, @{theory});
5.117 + ("xxx", "yyy", t, @{context});
5.118
5.119 (*if*) is_addUnordered arg;
5.120 "~~~~~ fun is_addUnordered , args:"; val (t) = (arg);
5.121 @@ -564,24 +564,24 @@
5.122 else error "poly.sml: diff.behav. in make_polynomial 23";
5.123 "-----SPO ---";
5.124 val t = TermC.str2term "a * b * b \<up> (- 1) + a";
5.125 -val SOME (t,_) = rewrite_set_ @{theory} false make_polynomial t; UnparseC.term t;
5.126 +val SOME (t,_) = rewrite_set_ @{context} false make_polynomial t; UnparseC.term t;
5.127 if UnparseC.term t = "2 * a" then ()
5.128 else error "poly.sml: diff.behav. in make_polynomial 25";
5.129 "-----SPO ---";
5.130 val t = TermC.str2term "a*c*b \<up> (2*n) + 3*a + 5*b \<up> (2*n)*c*b";
5.131 -val SOME (t,_) = rewrite_set_ @{theory} false make_polynomial t; UnparseC.term t;
5.132 +val SOME (t,_) = rewrite_set_ @{context} false make_polynomial t; UnparseC.term t;
5.133 if UnparseC.term t = "3 * a + 5 * b \<up> (1 + 2 * n) * c + a * b \<up> (2 * n) * c"
5.134 then () else error "poly.sml: diff.behav. in make_polynomial 26";
5.135
5.136 (*MG030627 -------------vvv-: Verschachtelte Terme -----------*)
5.137 "-----SPO ---";
5.138 val t = TermC.str2term "(1 + (x*y*a) + x) \<up> (1 + (x*y*a) + x)";
5.139 -val SOME (t,_) = rewrite_set_ @{theory} false make_polynomial t;
5.140 +val SOME (t,_) = rewrite_set_ @{context} false make_polynomial t;
5.141 if UnparseC.term t = "(1 + x + a * x * y) \<up> (1 + x + a * x * y)"
5.142 then () else error "poly.sml: diff.behav. in make_polynomial 27";(*SPO*)
5.143
5.144 val t = TermC.str2term "(1 + x*(y*z)*zz) \<up> (1 + x*(y*z)*zz)";
5.145 -val SOME (t,_) = rewrite_set_ @{theory} false make_polynomial t;
5.146 +val SOME (t,_) = rewrite_set_ @{context} false make_polynomial t;
5.147 if UnparseC.term t = "(1 + x * y * z * zz) \<up> (1 + x * y * z * zz)"
5.148 then () else error "poly.sml: diff.behav. in make_polynomial 28";
5.149
5.150 @@ -604,9 +604,7 @@
5.151 ... then Rewrite.trace_on:*)
5.152
5.153 "----- 2 ---";
5.154 -Rewrite.trace_on := false; (*true false*)
5.155 M_Match.match_pbl fmz pbt;
5.156 -Rewrite.trace_on := false; (*true false*)
5.157 (*... if there is no rewrite, then there is something wrong with prls*)
5.158
5.159 "-----3 ---";
5.160 @@ -695,12 +693,12 @@
5.161 val t1 = TermC.str2term "2 * b + (3 * a + 3 * b)";
5.162 val t2 = TermC.str2term "(3 * a + 3 * b) + 2 * b";
5.163
5.164 -if ord_make_polynomial true thy [] (t1, t2) then ()
5.165 +if ord_make_polynomial true @{theory} [] (t1, t2) then ()
5.166 else error "poly.sml: diff.behav. in ord_make_polynomial";
5.167 (*SO: WHY IS THERE NO REWRITING ...*)
5.168
5.169 val term = TermC.str2term "2*b + (3*a + 3*b)";
5.170 -(*+++*)val NONE = rewrite_set_ @{theory "Isac_Knowledge"} false order_add_mult term;
5.171 +(*+++*)val NONE = rewrite_set_ (Proof_Context.init_global @{theory "Isac_Knowledge"}) false order_add_mult term;
5.172 (*
5.173 WHY IS THERE NO REWRITING ?!?
5.174 most likely reason: Poly.thy and Rationa.thy do AC rewriting in ML,
6.1 --- a/test/Tools/isac/Test_Isac.thy Sat Aug 06 10:45:24 2022 +0200
6.2 +++ b/test/Tools/isac/Test_Isac.thy Sat Aug 06 15:02:55 2022 +0200
6.3 @@ -274,7 +274,7 @@
6.4 ML_file "Knowledge/descript.sml"
6.5 ML_file "Knowledge/simplify.sml"
6.6 ML_file "Knowledge/poly-1.sml"
6.7 -ML_file "Knowledge/poly-2.sml" (*Test_Isac_Short*)
6.8 + ML_file "Knowledge/poly-2.sml" (*Test_Isac_Short*)
6.9 ML_file "Knowledge/gcd_poly_ml.sml"
6.10 ML_file "Knowledge/rational-1.sml"
6.11 ML_file "Knowledge/rational-2.sml" (*Test_Isac_Short*)