1.1 --- a/test/Tools/isac/ProgLang/evaluate.sml Mon Nov 07 19:49:14 2022 +0100
1.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml Mon Nov 07 19:58:01 2022 +0100
1.3 @@ -120,7 +120,7 @@
1.4 ie. cancel does not work properly
1.5 *)
1.6 val thy = @{theory "Test"};
1.7 - val op_ = the (LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE"));
1.8 + val op_ = the (LibraryC.assoc (Know_Store.get_calcs @{theory}, "DIVIDE"));
1.9 val ct = @{term
1.10 "sqrt (x \<up> 2 + -3 * x) = (-9) / (- 2) + (-3 / (- 2) + (x * ((-4) / (- 2)) + x * (2 / (- 2))))"};
1.11 case calculate_ ctxt op_ ct of
1.12 @@ -225,32 +225,32 @@
1.13
1.14 val thy = @{theory Test};
1.15 val t = TermC.parseNEW' ctxt "12 / 3";
1.16 -val SOME (thmID,thm) = adhoc_thm ctxt(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"DIVIDE")))t;
1.17 +val SOME (thmID,thm) = adhoc_thm ctxt(the(LibraryC.assoc(Know_Store.get_calcs @{theory},"DIVIDE")))t;
1.18 val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t;
1.19 "12 / 3 = 4";
1.20 val thy = @{theory Test};
1.21 val t = TermC.parseNEW' ctxt "4 \<up> 2";
1.22 -val SOME (thmID,thm) = adhoc_thm ctxt(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"))) t;
1.23 +val SOME (thmID,thm) = adhoc_thm ctxt(the(LibraryC.assoc(Know_Store.get_calcs @{theory},"POWER"))) t;
1.24 val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t;
1.25 "4 ^ 2 = 16";
1.26
1.27 val t = TermC.parseNEW' ctxt "((1 + 2) * 4 / 3) \<up> 2";
1.28 - val SOME (thmID,thm) = adhoc_thm ctxt (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"PLUS"))) t;
1.29 + val SOME (thmID,thm) = adhoc_thm ctxt (the(LibraryC.assoc(Know_Store.get_calcs @{theory},"PLUS"))) t;
1.30 "1 + 2 = 3";
1.31 val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t;
1.32 UnparseC.term t;
1.33 "(3 * 4 / 3) \<up> 2";
1.34 - val SOME (thmID,thm) = adhoc_thm ctxt (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"TIMES")))t;
1.35 + val SOME (thmID,thm) = adhoc_thm ctxt (the(LibraryC.assoc(Know_Store.get_calcs @{theory},"TIMES")))t;
1.36 "3 * 4 = 12";
1.37 val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t;
1.38 UnparseC.term t;
1.39 "(12 / 3) \<up> 2";
1.40 - val SOME (thmID,thm) =adhoc_thm ctxt(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"DIVIDE")))t;
1.41 + val SOME (thmID,thm) =adhoc_thm ctxt(the(LibraryC.assoc(Know_Store.get_calcs @{theory},"DIVIDE")))t;
1.42 "12 / 3 = 4";
1.43 val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t;
1.44 UnparseC.term t;
1.45 "4 \<up> 2";
1.46 - val SOME (thmID,thm) = adhoc_thm ctxt(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER")))t;
1.47 + val SOME (thmID,thm) = adhoc_thm ctxt(the(LibraryC.assoc(Know_Store.get_calcs @{theory},"POWER")))t;
1.48 "4 \<up> 2 = 16";
1.49 val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t;
1.50 UnparseC.term t;
1.51 @@ -261,10 +261,10 @@
1.52 (*13.9.02 *** calc: operator = pow not defined*)
1.53 val t = TermC.parseNEW' ctxt "3 \<up> 2";
1.54 val SOME (thmID,thm) =
1.55 - adhoc_thm ctxt (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"))) t;
1.56 + adhoc_thm ctxt (the(LibraryC.assoc(Know_Store.get_calcs @{theory},"POWER"))) t;
1.57 (*** calc: operator = pow not defined*)
1.58
1.59 - val (op_, eval_fn) = the (LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"));
1.60 + val (op_, eval_fn) = the (LibraryC.assoc(Know_Store.get_calcs @{theory},"POWER"));
1.61 (*
1.62 val op_ = \<^const_name>\<open>realpow\<close> : string
1.63 val eval_fn = fn : string -> term -> theory -> (string * term) option*)
1.64 @@ -347,7 +347,7 @@
1.65 "----------- fun get_pair: examples ------------------------------------------------------------";
1.66 val thy = @{theory};
1.67 val ctxt = @{context};
1.68 -val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "PLUS");
1.69 +val SOME (isa_str, eval_fn) = LibraryC.assoc (Know_Store.get_calcs @{theory}, "PLUS");
1.70 if isa_str = "Groups.plus_class.plus" then () else error "eval_fn PLUS changed";
1.71
1.72 val t = @{term "3 + 4 :: real"};
1.73 @@ -370,14 +370,14 @@
1.74 if str = "#: 3 + (4 + a) = 7 + a" andalso UnparseC.term term = "3 + (4 + a) = 7 + a"
1.75 then ((* !!! gets subterm !!!*)) else error "get_pair x = 5 * (3 + (4 + a)) (subterm) changed";
1.76
1.77 -val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE");
1.78 +val SOME (isa_str, eval_fn) = LibraryC.assoc (Know_Store.get_calcs @{theory}, "DIVIDE");
1.79
1.80 val t = @{term "-4 / - 2 :: real"};
1.81 val SOME (str, term) = get_pair ctxt isa_str eval_fn t;
1.82 if str = "#divide_e~4_~2" andalso UnparseC.term term = "- 4 / - 2 = 2"
1.83 then () else error "get_pair -4 / - 2 changed";
1.84
1.85 -val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "POWER");
1.86 +val SOME (isa_str, eval_fn) = LibraryC.assoc (Know_Store.get_calcs @{theory}, "POWER");
1.87
1.88 val t = @{term "2 \<up> 3 :: real"};
1.89 val SOME (str, term) = get_pair ctxt isa_str eval_fn t;
1.90 @@ -388,7 +388,7 @@
1.91 "----------- fun adhoc_thm: examples -----------------------------------------------------------";
1.92 "----------- fun adhoc_thm: examples -----------------------------------------------------------";
1.93 (*--------------------------------------------------------------------vvvvvvvvvv*)
1.94 -val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "is_num");
1.95 +val SOME (isa_str, eval_fn) = LibraryC.assoc (Know_Store.get_calcs @{theory}, "is_num");
1.96 val t = @{term "9 is_num"};
1.97 val SOME (str, thm) = adhoc_thm ctxt (isa_str, eval_fn) t;
1.98 if str = "#is_num_9_" andalso ThmC_Def.string_of_thm thm = "(9 is_num) = True"
1.99 @@ -396,7 +396,7 @@
1.100
1.101 case get_calc_prog_id ctxt \<^const_name>\<open>less\<close> of
1.102 "le" => () | _ => error "Orderings.ord_class.less <-> le changed";
1.103 -val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "le");
1.104 +val SOME (isa_str, eval_fn) = LibraryC.assoc (Know_Store.get_calcs @{theory}, "le");
1.105 if isa_str = "Orderings.ord_class.less" then () else error "adhoc_thm (4 < 4) = False CHANGED";
1.106
1.107 val t = @{term "4 < (4 :: real)"};
1.108 @@ -408,13 +408,13 @@
1.109 case adhoc_thm ctxt (isa_str, eval_fn) t of
1.110 NONE => () | _ => error "adhoc_thm a < 4 does NOT result in NONE";
1.111
1.112 -val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "PLUS");
1.113 +val SOME (isa_str, eval_fn) = LibraryC.assoc (Know_Store.get_calcs @{theory}, "PLUS");
1.114 val SOME t = parseNEW @{context} "1 + (2::real)";
1.115 val SOME (str, thm) = adhoc_thm ctxt (isa_str, eval_fn) t;
1.116 if str = "#: 1 + 2 = 3" andalso ThmC_Def.string_of_thm thm = "1 + 2 = 3"
1.117 then () else error "adhoc_thm 1 + 2 changed";
1.118
1.119 -val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE");
1.120 +val SOME (isa_str, eval_fn) = LibraryC.assoc (Know_Store.get_calcs @{theory}, "DIVIDE");
1.121 val t = @{term "6 / -8 :: real"};
1.122 val SOME (str, thm) = adhoc_thm ctxt (isa_str, eval_fn) t;
1.123 if str = "#divide_e6_~8" andalso ThmC_Def.string_of_thm thm = "6 / - 8 = - 3 / 4"
1.124 @@ -422,7 +422,7 @@
1.125
1.126 case get_calc_prog_id ctxt "Prog_Expr.ident" of
1.127 "ident" => () | _ => error "Prog_Expr.ident <-> ident changed";
1.128 -val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "ident");
1.129 +val SOME (isa_str, eval_fn) = LibraryC.assoc (Know_Store.get_calcs @{theory}, "ident");
1.130
1.131 val t = @{term "3 =!= (3 :: real)"};
1.132 val SOME (str, thm) = adhoc_thm ctxt (isa_str, eval_fn) t;