1.1 --- a/test/Tools/isac/ProgLang/evaluate.sml Mon Apr 19 20:44:18 2021 +0200
1.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml Tue Apr 20 16:58:44 2021 +0200
1.3 @@ -43,7 +43,7 @@
1.4 "----------- fun calculate_ --------------------------------------------------------------------";
1.5 "----------- fun calculate_ --------------------------------------------------------------------";
1.6 (* fun rewrite__set_ \<longrightarrow> fun rew_once works the same way *)
1.7 -val t = TermC.str2term "((1+2)*4/3)^^^2";
1.8 +val t = TermC.str2term "((1+2)*4/3) \<up> 2";
1.9 val thy = @{theory};
1.10 val times = ("Groups.times_class.times", eval_binop "#mult_") : string * Eval_Def.eval_fn;
1.11 val plus = ("Groups.plus_class.plus",eval_binop "#add_") : string * Eval_Def.eval_fn;
1.12 @@ -53,20 +53,20 @@
1.13 "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, plus, t);
1.14 val SOME ("#: 1 + 2 = 3", adh_thm) = adhoc_thm @{theory} isa_fn t;
1.15 val SOME (t', []) = rewrite__ thy 0 [] e_rew_ord Rule_Set.empty true adh_thm t;
1.16 -if UnparseC.term t' = "(3 * 4 / 3) ^^^ 2" then () else error "calculate_ 1 + 2 = 3 changed";
1.17 +if UnparseC.term t' = "(3 * 4 / 3) \<up> 2" then () else error "calculate_ 1 + 2 = 3 changed";
1.18
1.19 "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, times, t');
1.20 val SOME ("#: 3 * 4 = 12", adh_thm) = adhoc_thm @{theory} isa_fn t';
1.21 val SOME (t'', []) = rewrite__ thy 0 [] e_rew_ord Rule_Set.empty true adh_thm t;
1.22 -if UnparseC.term t'' = "(12 / 3) ^^^ 2" then () else error "calculate_ 3 * 4 = 12 changed";
1.23 +if UnparseC.term t'' = "(12 / 3) \<up> 2" then () else error "calculate_ 3 * 4 = 12 changed";
1.24
1.25 "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, divide, t'');
1.26 val SOME ("#divide_e12_3", adh_thm) = adhoc_thm @{theory} isa_fn t;
1.27 val SOME (t''', []) = rewrite__ thy 0 [] e_rew_ord Rule_Set.empty true adh_thm t;
1.28 -if UnparseC.term t''' = "4 ^^^ 2" then () else error "calculate_ 12 / 3 = 4 changed";
1.29 +if UnparseC.term t''' = "4 \<up> 2" then () else error "calculate_ 12 / 3 = 4 changed";
1.30
1.31 "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, pow, t''');
1.32 -val SOME ("#: 4 ^^^ 2 = 16", adh_thm) = adhoc_thm @{theory} isa_fn t;
1.33 +val SOME ("#: 4 \<up> 2 = 16", adh_thm) = adhoc_thm @{theory} isa_fn t;
1.34 val SOME (t'''', []) = rewrite__ thy 0 [] e_rew_ord Rule_Set.empty true adh_thm t;
1.35 if UnparseC.term t'''' = "16" then () else error "calculate_ 12 / 3 = 4 changed";
1.36
1.37 @@ -74,13 +74,13 @@
1.38 "----------- calculate from Prog --------------------------------- -----------------------------";
1.39 "----------- calculate from Prog --------------------------------- -----------------------------";
1.40 val thy = @{theory "Test"};
1.41 -val fmz = ["realTestGiven (((1+2)*4/3)^^^2)", "realTestFind s"];
1.42 +val fmz = ["realTestGiven (((1+2)*4/3) \<up> 2)", "realTestFind s"];
1.43 val (dI',pI',mI') =
1.44 ("Test",["calculate", "test"],["Test", "test_calculate"]);
1.45
1.46 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.47 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.48 -(*nxt =("Add_Given",Add_Given "realTestGiven (((#1 + #2) * #4 // #3) ^^^#2)")*)
1.49 +(*nxt =("Add_Given",Add_Given "realTestGiven (((#1 + #2) * #4 // #3) \<up> #2)")*)
1.50 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.51 (*nxt = ("Add_Find",Add_Find "realTestFind s") : string * tac*)
1.52 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.53 @@ -107,22 +107,22 @@
1.54 "----------- calculate check test-root-equ --------------";
1.55 (*(1): 2nd Test_simplify didn't work:
1.56 val ct =
1.57 - "sqrt (x ^^^ 2 + -3 * x) = (-3 + 2 * x + -1 * (9 + 4 * x)) / (-1 * 2)"
1.58 + "sqrt (x \<up> 2 + -3 * x) = (-3 + 2 * x + -1 * (9 + 4 * x)) / (-1 * 2)"
1.59 > val rls = ("Test_simplify");
1.60 > val (ct,_) = the (rewrite_set thy' ("tval_rls") false rls ct);
1.61 -val ct = "sqrt (x ^^^ 2 + -3 * x) =
1.62 +val ct = "sqrt (x \<up> 2 + -3 * x) =
1.63 (-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))";
1.64 ie. cancel does not work properly
1.65 *)
1.66 val thy = @{theory "Test"};
1.67 val op_ = the (LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE"));
1.68 val ct = ThmC_Def.num_to_Free @{term
1.69 - "sqrt (x ^^^ 2 + -3 * x) = (-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))"};
1.70 + "sqrt (x \<up> 2 + -3 * x) = (-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))"};
1.71 case calculate_ thy op_ ct of
1.72 SOME _ => ()
1.73 | NONE => error "calculate_ test-root-equ changed";
1.74 (*
1.75 - sqrt (x ^^^ 2 + -3 * x) =\
1.76 + sqrt (x \<up> 2 + -3 * x) =\
1.77 \(-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))
1.78 ............... does not work *)
1.79
1.80 @@ -227,7 +227,7 @@
1.81 *** . Free ( 1, 'a)
1.82 *** . Free ( aaa, nat) *)
1.83
1.84 -val t = TermC.str2term "1 ^^^ aaa";
1.85 +val t = TermC.str2term "1 \<up> aaa";
1.86 TermC.atomty t;
1.87 (****
1.88 *** Const (Prog_Expr.pow, real => real => real)
1.89 @@ -245,29 +245,29 @@
1.90 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.91 "12 / 3 = 4";
1.92 val thy = @{theory Test};
1.93 -val t = (Thm.term_of o the o (TermC.parse thy)) "4 ^^^ 2";
1.94 +val t = (Thm.term_of o the o (TermC.parse thy)) "4 \<up> 2";
1.95 val SOME (thmID,thm) = adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"))) t;
1.96 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.97 "4 ^ 2 = 16";
1.98
1.99 - val t = (Thm.term_of o the o (TermC.parse thy)) "((1 + 2) * 4 / 3) ^^^ 2";
1.100 + val t = (Thm.term_of o the o (TermC.parse thy)) "((1 + 2) * 4 / 3) \<up> 2";
1.101 val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"PLUS"))) t;
1.102 "1 + 2 = 3";
1.103 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.104 UnparseC.term t;
1.105 -"(3 * 4 / 3) ^^^ 2";
1.106 +"(3 * 4 / 3) \<up> 2";
1.107 val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"TIMES")))t;
1.108 "3 * 4 = 12";
1.109 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.110 UnparseC.term t;
1.111 -"(12 / 3) ^^^ 2";
1.112 +"(12 / 3) \<up> 2";
1.113 val SOME (thmID,thm) =adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"DIVIDE")))t;
1.114 "12 / 3 = 4";
1.115 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.116 UnparseC.term t;
1.117 -"4 ^^^ 2";
1.118 +"4 \<up> 2";
1.119 val SOME (thmID,thm) = adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER")))t;
1.120 -"4 ^^^ 2 = 16";
1.121 +"4 \<up> 2 = 16";
1.122 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.123 UnparseC.term t;
1.124 "16";
1.125 @@ -275,7 +275,7 @@
1.126 else ();
1.127
1.128 (*13.9.02 *** calc: operator = pow not defined*)
1.129 - val t = (Thm.term_of o the o (TermC.parse thy)) "3^^^2";
1.130 + val t = (Thm.term_of o the o (TermC.parse thy)) "3 \<up> 2";
1.131 val SOME (thmID,thm) =
1.132 adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"))) t;
1.133 (*** calc: operator = pow not defined*)
1.134 @@ -303,11 +303,11 @@
1.135 (thy, "EqSystem.occur'_exactly'_in",
1.136 assoc_calc' (@{theory "EqSystem"}) "occur_exactly_in" |> snd |> snd,
1.137 TermC.str2term
1.138 - "[] from [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L ^^^ 2) / 2"
1.139 + "[] from [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L \<up> 2) / 2"
1.140 );
1.141 val SOME (str, simpl) = get_pair thy op_ ef arg;
1.142 if str =
1.143 -"[] from [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L ^^^ 2) / 2 = True"
1.144 +"[] from [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L \<up> 2) / 2 = True"
1.145 then () else error "evaluate.sml get_pair with 3 args:occur_exactly_in";
1.146
1.147
1.148 @@ -358,10 +358,10 @@
1.149
1.150 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "POWER");
1.151
1.152 -val t = (Thm.term_of o the o (TermC.parse thy)) "2 ^^^ 3";
1.153 +val t = (Thm.term_of o the o (TermC.parse thy)) "2 \<up> 3";
1.154 val SOME (str, term) = get_pair thy isa_str eval_fn t;
1.155 -if str = "#: 2 ^^^ 3 = 8" andalso UnparseC.term term = "2 ^^^ 3 = 8"
1.156 -then () else error "get_pair 2 ^^^ 3 changed";
1.157 +if str = "#: 2 \<up> 3 = 8" andalso UnparseC.term term = "2 \<up> 3 = 8"
1.158 +then () else error "get_pair 2 \<up> 3 changed";
1.159
1.160 "----------- fun adhoc_thm: examples -----------------------------------------------------------";
1.161 "----------- fun adhoc_thm: examples -----------------------------------------------------------";