1.1 --- a/test/Tools/isac/ProgLang/evaluate.sml Tue Jul 20 14:37:56 2021 +0200
1.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml Tue Jul 27 11:21:14 2021 +0200
1.3 @@ -129,13 +129,13 @@
1.4
1.5 (*--------------(2): does divide work in Test_simplify ?: ------*)
1.6 val thy = @{theory Test};
1.7 - val t = TermC.parseNEW'' thy "6 / 2";
1.8 + val t = (Thm.term_of o the o (TermC.parse thy)) "6 / 2";
1.9 val rls = Test_simplify;
1.10 val (t,_) = the (rewrite_set_ thy false rls t);
1.11 (*val t = Free ("3", "Real.real") : term*)
1.12
1.13 (*--------------(3): is_const works ?: -------------------------------------*)
1.14 - val t = TermC.parseNEW'' thy "2 is_const";
1.15 + val t = (Thm.term_of o the o (TermC.parse @{theory Test})) "2 is_const";
1.16 TermC.atomty t;
1.17 rewrite_set_ @{theory Test} false tval_rls t;
1.18 (*val it = SOME (Const (\<^const_name>\<open>True\<close>, "bool"),[]) ... works*)
1.19 @@ -152,19 +152,19 @@
1.20 Rewrite.trace_on := false; (*true false*)
1.21 val thy = @{theory Test};
1.22 val rls = Test_simplify;
1.23 - val t = TermC.parseNEW'' thy "(-4) / 2";
1.24 + val t = (Thm.term_of o the o (TermC.parse thy)) "(-4) / 2";
1.25
1.26 val SOME (_, t) = eval_cancel "xxx" \<^const_name>\<open>divide\<close> t thy;
1.27
1.28 (*--------------(5): reproduce (1) with simpler term: ------------*)
1.29 - val t = TermC.parseNEW'' thy "(3+5)/2::real";
1.30 + val t = (Thm.term_of o the o (TermC.parse thy)) "(3+5)/2";
1.31 case rewrite_set_ thy false rls t of
1.32 SOME (t', []) =>
1.33 if UnparseC.term t' = "4" then ()
1.34 else error "rewrite_set_ (3+5)/2 changed 1"
1.35 | _ => error "rewrite_set_ (3+5)/2 changed 2";
1.36
1.37 - val t = TermC.parseNEW'' thy "(3+1+2*x)/2::real";
1.38 + val t = (Thm.term_of o the o (TermC.parse thy)) "(3+1+2*x)/2";
1.39 case rewrite_set_ thy false rls t of
1.40 SOME (t', _) => (*WAS "x + 2" WITH OLD numerals TOODOO?*)
1.41 if UnparseC.term t' = "2 + x" then () else error "rewrite_set_ (3+1+2*x)/2 changed 1"
1.42 @@ -202,7 +202,7 @@
1.43
1.44 (*===================*)
1.45 Rewrite.trace_on:=false; (*WN130722: =true stopped Test_Isac.thy*)
1.46 - val t = TermC.parseNEW'' thy "x + (- 1 + -3) / 2::real";
1.47 + val t = (Thm.term_of o the o (TermC.parse thy)) "x + (- 1 + -3) / 2";
1.48 val SOME (res, []) = rewrite_set_ thy false rls t;
1.49 (*WAS "x + - 2" WITH OLD numerals TOODOO?*)
1.50 if UnparseC.term res = "- 2 + x" then () else error "rewrite_set_ x + (- 1 + -3) / 2 changed";
1.51 @@ -227,17 +227,17 @@
1.52 " ================= evaluate.sml: calculate_ 2002 =================== ";
1.53
1.54 val thy = @{theory Test};
1.55 -val t = TermC.parseNEW'' thy "12 / 3";
1.56 +val t = (Thm.term_of o the o (TermC.parse thy)) "12 / 3";
1.57 val SOME (thmID,thm) = adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"DIVIDE")))t;
1.58 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.59 "12 / 3 = 4";
1.60 val thy = @{theory Test};
1.61 -val t = TermC.parseNEW'' thy "4 \<up> 2";
1.62 +val t = (Thm.term_of o the o (TermC.parse thy)) "4 \<up> 2";
1.63 val SOME (thmID,thm) = adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"))) t;
1.64 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.65 "4 ^ 2 = 16";
1.66
1.67 - val t = TermC.parseNEW'' thy "((1 + 2) * 4 / 3) \<up> 2";
1.68 + val t = (Thm.term_of o the o (TermC.parse thy)) "((1 + 2) * 4 / 3) \<up> 2";
1.69 val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"PLUS"))) t;
1.70 "1 + 2 = 3";
1.71 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.72 @@ -262,7 +262,7 @@
1.73 else ();
1.74
1.75 (*13.9.02 *** calc: operator = pow not defined*)
1.76 - val t = TermC.parseNEW'' thy "3 \<up> 2";
1.77 + val t = (Thm.term_of o the o (TermC.parse thy)) "3 \<up> 2";
1.78 val SOME (thmID,thm) =
1.79 adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"))) t;
1.80 (*** calc: operator = pow not defined*)