1.1 --- a/test/Tools/isac/ProgLang/evaluate.sml Mon Apr 19 11:45:43 2021 +0200
1.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml Mon Apr 19 15:02:00 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 = str2term "((1+2)*4/3)^^^2";
1.8 +val t = TermC.str2term "((1+2)*4/3)^^^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 @@ -128,18 +128,18 @@
1.13
1.14 (*--------------(2): does divide work in Test_simplify ?: ------*)
1.15 val thy = @{theory Test};
1.16 - val t = (Thm.term_of o the o (parse thy)) "6 / 2";
1.17 + val t = (Thm.term_of o the o (TermC.parse thy)) "6 / 2";
1.18 val rls = Test_simplify;
1.19 val (t,_) = the (rewrite_set_ thy false rls t);
1.20 (*val t = Free ("3", "Real.real") : term*)
1.21
1.22 (*--------------(3): is_const works ?: -------------------------------------*)
1.23 - val t = (Thm.term_of o the o (parse @{theory Test})) "2 is_const";
1.24 - atomty t;
1.25 + val t = (Thm.term_of o the o (TermC.parse @{theory Test})) "2 is_const";
1.26 + TermC.atomty t;
1.27 rewrite_set_ @{theory Test} false tval_rls t;
1.28 (*val it = SOME (Const ("HOL.True", "bool"),[]) ... works*)
1.29
1.30 - val t = str2term "2 * x is_const";
1.31 + val t = TermC.str2term "2 * x is_const";
1.32 val SOME (str,t') = eval_const "" "" t (@{theory "Isac_Knowledge"});
1.33 UnparseC.term t';
1.34
1.35 @@ -151,17 +151,17 @@
1.36 Rewrite.trace_on := false;
1.37 val thy = @{theory Test};
1.38 val rls = Test_simplify;
1.39 - val t = (Thm.term_of o the o (parse thy)) "(-4) / 2";
1.40 + val t = (Thm.term_of o the o (TermC.parse thy)) "(-4) / 2";
1.41
1.42 val SOME (_, t) = eval_cancel "xxx" "Rings.divide_class.divide" t thy;
1.43
1.44 (*--------------(5): reproduce (1) with simpler term: ------------*)
1.45 - val t = (Thm.term_of o the o (parse thy)) "(3+5)/2";
1.46 + val t = (Thm.term_of o the o (TermC.parse thy)) "(3+5)/2";
1.47 case rewrite_set_ thy false rls t of
1.48 SOME (Free ("4", _), []) => ()
1.49 | _ => error "rewrite_set_ (3+5)/2 changed";
1.50
1.51 - val t = (Thm.term_of o the o (parse thy)) "(3+1+2*x)/2";
1.52 + val t = (Thm.term_of o the o (TermC.parse thy)) "(3+1+2*x)/2";
1.53 case rewrite_set_ thy false rls t of
1.54 SOME (Const ("Groups.plus_class.plus", _) $ Free ("2", _) $ Free ("x", _), []) => ()
1.55 | _ => error "rewrite_set_ (3+1+2*x)/2 changed";
1.56 @@ -198,7 +198,7 @@
1.57
1.58 (*===================*)
1.59 Rewrite.trace_on:=false; (*WN130722: =true stopped Test_Isac.thy*)
1.60 - val t = (Thm.term_of o the o (parse thy)) "x + (-1 + -3) / 2";
1.61 + val t = (Thm.term_of o the o (TermC.parse thy)) "x + (-1 + -3) / 2";
1.62 val SOME (res, []) = rewrite_set_ thy false rls t;
1.63 if UnparseC.term res = "-2 + x" then () else error "rewrite_set_ x + (-1 + -3) / 2 changed";
1.64 "x + (-4) / 2";
1.65 @@ -221,14 +221,14 @@
1.66 "----------- Prog_Expr.pow Power.power_class.power ---------";
1.67 "----------- Prog_Expr.pow Power.power_class.power ---------";
1.68 val t = (Thm.term_of o the o (parseold thy)) "1 ^ aaa";
1.69 -atomty t;
1.70 +TermC.atomty t;
1.71 (*** -------------
1.72 *** Const ( Nat.power, ['a, nat] => 'a)
1.73 *** . Free ( 1, 'a)
1.74 *** . Free ( aaa, nat) *)
1.75
1.76 -val t = str2term "1 ^^^ aaa";
1.77 -atomty t;
1.78 +val t = TermC.str2term "1 ^^^ aaa";
1.79 +TermC.atomty t;
1.80 (****
1.81 *** Const (Prog_Expr.pow, real => real => real)
1.82 *** . Free (1, real)
1.83 @@ -240,17 +240,17 @@
1.84 " ================= evaluate.sml: calculate_ 2002 =================== ";
1.85
1.86 val thy = @{theory Test};
1.87 -val t = (Thm.term_of o the o (parse thy)) "12 / 3";
1.88 +val t = (Thm.term_of o the o (TermC.parse thy)) "12 / 3";
1.89 val SOME (thmID,thm) = adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"DIVIDE")))t;
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 (parse thy)) "4 ^^^ 2";
1.94 +val t = (Thm.term_of o the o (TermC.parse thy)) "4 ^^^ 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 (parse thy)) "((1 + 2) * 4 / 3) ^^^ 2";
1.100 + val t = (Thm.term_of o the o (TermC.parse thy)) "((1 + 2) * 4 / 3) ^^^ 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 @@ -275,7 +275,7 @@
1.105 else ();
1.106
1.107 (*13.9.02 *** calc: operator = pow not defined*)
1.108 - val t = (Thm.term_of o the o (parse thy)) "3^^^2";
1.109 + val t = (Thm.term_of o the o (TermC.parse thy)) "3^^^2";
1.110 val SOME (thmID,thm) =
1.111 adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"))) t;
1.112 (*** calc: operator = pow not defined*)
1.113 @@ -302,7 +302,7 @@
1.114 val (thy, op_, ef, arg) =
1.115 (thy, "EqSystem.occur'_exactly'_in",
1.116 assoc_calc' (@{theory "EqSystem"}) "occur_exactly_in" |> snd |> snd,
1.117 - str2term
1.118 + TermC.str2term
1.119 "[] from [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L ^^^ 2) / 2"
1.120 );
1.121 val SOME (str, simpl) = get_pair thy op_ ef arg;
1.122 @@ -314,7 +314,7 @@
1.123 "----------- calculate (2 * x is_const) -----------------";
1.124 "----------- calculate (2 * x is_const) -----------------";
1.125 "----------- calculate (2 * x is_const) -----------------";
1.126 -val t = str2term "2 * x is_const";
1.127 +val t = TermC.str2term "2 * x is_const";
1.128 val SOME (str, t') = eval_const "" "" t @{theory Test};
1.129 UnparseC.term t';
1.130 "(2 * x is_const) = False";
1.131 @@ -329,36 +329,36 @@
1.132 val thy = @{theory};
1.133 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "PLUS");
1.134
1.135 -val t = (Thm.term_of o the o (parse thy)) "3 + 4";
1.136 +val t = (Thm.term_of o the o (TermC.parse thy)) "3 + 4";
1.137 val SOME (str, term) = get_pair thy isa_str eval_fn t;
1.138 if str = "#: 3 + 4 = 7" andalso UnparseC.term term = "3 + 4 = 7"
1.139 then () else error "get_pair 3 + 4 changed";
1.140
1.141 -val t = (Thm.term_of o the o (parse thy)) "(a + 3) + 4";
1.142 +val t = (Thm.term_of o the o (TermC.parse thy)) "(a + 3) + 4";
1.143 val SOME (str, term) = get_pair thy isa_str eval_fn t;
1.144 if str = "#: a + 3 + 4 = a + 7" andalso UnparseC.term term = "a + 3 + 4 = a + 7"
1.145 then () else error "get_pair (a + 3) + 4 changed";
1.146
1.147 -val t = (Thm.term_of o the o (parse thy)) "(a + 3) + 4";
1.148 +val t = (Thm.term_of o the o (TermC.parse thy)) "(a + 3) + 4";
1.149 val SOME (str, term) = get_pair thy isa_str eval_fn t;
1.150 if str = "#: a + 3 + 4 = a + 7" andalso UnparseC.term term = "a + 3 + 4 = a + 7"
1.151 then () else error "get_pair (a + 3) + 4 changed";
1.152
1.153 -val t = (Thm.term_of o the o (parse thy)) "x = 5 * (3 + (4 + a))";
1.154 +val t = (Thm.term_of o the o (TermC.parse thy)) "x = 5 * (3 + (4 + a))";
1.155 val SOME (str, term) = get_pair thy isa_str eval_fn t;
1.156 if str = "#: 3 + (4 + a) = 7 + a" andalso UnparseC.term term = "3 + (4 + a) = 7 + a"
1.157 then ((* !!! gets subterm !!!*)) else error "get_pair x = 5 * (3 + (4 + a)) (subterm) changed";
1.158
1.159 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE");
1.160
1.161 -val t = (Thm.term_of o the o (parse thy)) "-4 / -2";
1.162 +val t = (Thm.term_of o the o (TermC.parse thy)) "-4 / -2";
1.163 val SOME (str, term) = get_pair thy isa_str eval_fn t;
1.164 if str = "#divide_e-4_-2" andalso UnparseC.term term = "-4 / -2 = 2"
1.165 then () else error "get_pair -4 / -2 changed";
1.166
1.167 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "POWER");
1.168
1.169 -val t = (Thm.term_of o the o (parse thy)) "2 ^^^ 3";
1.170 +val t = (Thm.term_of o the o (TermC.parse thy)) "2 ^^^ 3";
1.171 val SOME (str, term) = get_pair thy isa_str eval_fn t;
1.172 if str = "#: 2 ^^^ 3 = 8" andalso UnparseC.term term = "2 ^^^ 3 = 8"
1.173 then () else error "get_pair 2 ^^^ 3 changed";