1.1 --- a/test/Tools/isac/ProgLang/prog_expr.sml Sun Oct 09 06:53:03 2022 +0200
1.2 +++ b/test/Tools/isac/ProgLang/prog_expr.sml Sun Oct 09 07:44:22 2022 +0200
1.3 @@ -58,7 +58,7 @@
1.4 "-------- fun eval_is_even ---------------------------------------------------------------------";
1.5 "-------- fun eval_is_even ---------------------------------------------------------------------";
1.6 "-------- fun eval_is_even ---------------------------------------------------------------------";
1.7 -val t = TermC.str2term "2 is_even";
1.8 +val t = TermC.parse_test @{context} "2 is_even";
1.9 eval_is_even "aaa" "Prog_Expr.is_even" t "ccc";
1.10 "~~~~~ fun eval_is_even , args:"; val ((thmid:string), "Prog_Expr.is_even", (t as (Const _ $ arg)), _) =
1.11 ("aaa", "Prog_Expr.is_even", t, "ccc");
1.12 @@ -71,14 +71,14 @@
1.13 if UnparseC.term t' = "(2 is_even) = True" then () else error "(2 is_even) = True CHANGED";
1.14
1.15
1.16 -val t = TermC.str2term "3 is_even";
1.17 +val t = TermC.parse_test @{context} "3 is_even";
1.18 case eval_is_even "aaa" "Prog_Expr.is_even" t "ccc" of
1.19 SOME (str, t') =>
1.20 if str = "aaa_" andalso UnparseC.term t' = "(3 is_even) = False" then ()
1.21 else error "eval_is_even (3 is_even) CHANGED 1"
1.22 | NONE => error "eval_is_even (3 is_even) CHANGED 2";
1.23
1.24 -val t = TermC.str2term "a ::real";
1.25 +val t = TermC.parse_test @{context} "a ::real";
1.26 val NONE =
1.27 eval_is_even "aaa" "Prog_Expr.is_even" t "ccc";
1.28 case eval_is_even "aaa" "Prog_Expr.is_even" t "ccc" of
1.29 @@ -95,27 +95,27 @@
1.30 SOME (Const (\<^const_name>\<open>True\<close>, _), []) => ()
1.31 | _ => error "2 is_num CHANGED";
1.32
1.33 -val t = TermC.str2term "2 * x is_num";
1.34 +val t = TermC.parse_test @{context} "2 * x is_num";
1.35 val SOME (str, t') = eval_is_num "" "Prog_Expr.is_num" t (@{theory "Isac_Knowledge"});
1.36 if UnparseC.term t' = "(2 * x is_num) = False" then ()
1.37 else error "(2 * x is_num) = False CHANGED";
1.38
1.39 -val t = TermC.str2term "- 2 is_num";
1.40 +val t = TermC.parse_test @{context} "- 2 is_num";
1.41 val SOME (str, t') = eval_is_num "" "Prog_Expr.is_num" t (@{theory "Isac_Knowledge"});
1.42 if UnparseC.term t' = "(- 2 is_num) = True" then ()
1.43 else error "(- 2 is_num) = False CHANGED";
1.44
1.45 -val t = TermC.str2term "- 1 is_num";
1.46 +val t = TermC.parse_test @{context} "- 1 is_num";
1.47 val SOME (str, t') = eval_is_num "" "Prog_Expr.is_num" t (@{theory "Isac_Knowledge"});
1.48 if UnparseC.term t' = "(- 1 is_num) = True" then ()
1.49 else error "(- 1 is_num) = False CHANGED";
1.50
1.51 -val t = TermC.str2term "0 is_num";
1.52 +val t = TermC.parse_test @{context} "0 is_num";
1.53 val SOME (str, t') = eval_is_num "" "Prog_Expr.is_num" t (@{theory "Isac_Knowledge"});
1.54 if UnparseC.term t' = "(0 is_num) = True" then ()
1.55 else error "(0 is_num) = False CHANGED";
1.56
1.57 -val t = TermC.str2term "AA is_num";
1.58 +val t = TermC.parse_test @{context} "AA is_num";
1.59 val SOME (str, t') = eval_is_num "" "Prog_Expr.is_num" t (@{theory "Isac_Knowledge"});
1.60 if UnparseC.term t' = "(AA is_num) = False" then ()
1.61 else error "(0 is_num) = False CHANGED";
1.62 @@ -204,20 +204,20 @@
1.63 val thy = @{theory}
1.64 val ctxt = (ThyC.id_to_ctxt "Isac_Knowledge")
1.65
1.66 -val t = TermC.str2term "x = 0";
1.67 +val t = TermC.parse_test @{context} "x = 0";
1.68 val NONE(*= indetermined*) = eval_equal "equal_" \<^const_name>\<open>HOL.eq\<close> t ctxt;
1.69
1.70 -val t = TermC.str2term "(x + 1) = (x + 1)";
1.71 +val t = TermC.parse_test @{context} "(x + 1) = (x + 1)";
1.72 val (Const _(*op0,t0*) $ t1 $ t2 ) = t
1.73 val SOME ("equal_(x + 1)_(x + 1)", t') = eval_equal "equal_" \<^const_name>\<open>HOL.eq\<close> t ctxt;
1.74 if UnparseC.term t' = "(x + 1 = x + 1) = True" then () else error "(x + 1) = (x + 1) CHANGED";
1.75
1.76 -val t as Const _ $ v $ c = TermC.str2term "1 = 0";
1.77 +val t as Const _ $ v $ c = TermC.parse_test @{context} "1 = 0";
1.78 val false = variable_constant_pair (v, c);
1.79 val SOME ("equal_(1)_(0)", t') = eval_equal "equal_" \<^const_name>\<open>HOL.eq\<close> t ctxt;
1.80 if UnparseC.term t' = "(1 = 0) = False" then () else error "1 = 0 CHANGED";
1.81
1.82 -val t = TermC.str2term "0 = 0";
1.83 +val t = TermC.parse_test @{context} "0 = 0";
1.84 val SOME ("equal_(0)_(0)", t') = eval_equal "equal_" \<^const_name>\<open>HOL.eq\<close> t ctxt;
1.85 if UnparseC.term t' = "(0 = 0) = True" then () else error "0 = 0 CHANGED";
1.86
1.87 @@ -228,7 +228,7 @@
1.88 val t = @{term "x::real"};
1.89 if occurs_in t t then "OK" else error "occurs_in x x -> f ..changed";
1.90
1.91 -val t = TermC.str2term "x occurs_in x";
1.92 +val t = TermC.parse_test @{context} "x occurs_in x";
1.93 val SOME (str, t') = eval_occurs_in 0 "Prog_Expr.occurs_in" t 0;
1.94 if UnparseC.term t' = "x occurs_in x = True" then ()
1.95 else error "x occurs_in x = True ..changed";
1.96 @@ -337,7 +337,7 @@
1.97 "---------fun eval_argument_of -----------------------------------------------------------------";
1.98 "---------fun eval_argument_of -----------------------------------------------------------------";
1.99 "---------fun eval_argument_of -----------------------------------------------------------------";
1.100 -val t = TermC.str2term "argument_in (M_b x)";
1.101 +val t = TermC.parse_test @{context} "argument_in (M_b x)";
1.102 val SOME (str, t') = eval_argument_in "0" "Prog_Expr.argument_in" t 0;
1.103 if UnparseC.term t' = "(argument_in M_b x) = x" then ()
1.104 else error "atools.sml:(argument_in M_b x) = x ???";
1.105 @@ -450,10 +450,10 @@
1.106 "-------- fun matchsub -------------------------------------------------------------------------";
1.107 "-------- fun matchsub -------------------------------------------------------------------------";
1.108 "-------- fun matchsub -------------------------------------------------------------------------";
1.109 -if matchsub thy (TermC.str2term "(a + (b + c))") (TermC.str2term "?x + (?y + ?z)")
1.110 +if matchsub thy (TermC.parse_test @{context} "(a + (b + c))") (TermC.parse_patt_test @{theory} "?x + (?y + ?z)")
1.111 then () else error "tools.sml matchsub a + (b + c)";
1.112
1.113 -if matchsub thy (TermC.str2term "(a + (b + c)) + d") (TermC.str2term "?x + (?y + ?z)")
1.114 +if matchsub thy (TermC.parse_test @{context} "(a + (b + c)) + d") (TermC.parse_patt_test @{theory} "?x + (?y + ?z)")
1.115 then () else error "tools.sml matchsub (a + (b + c)) + d";
1.116
1.117
1.118 @@ -465,9 +465,9 @@
1.119 | _ => error "TermC.UniversalList changed 1";
1.120 case or2list @{term False} of Const (\<^const_name>\<open>Nil\<close>, _) => ()
1.121 | _ => error "TermC.UniversalList changed 2";
1.122 -val t = (TermC.str2term "x=3");
1.123 +val t = (TermC.parse_test @{context} "x=3");
1.124 if UnparseC.term (or2list t) = "[x = 3]" then ()
1.125 else error "or2list changed";
1.126 -val t = (TermC.str2term "x=3 | x=-3 | x=0");
1.127 +val t = (TermC.parse_test @{context} "x=3 | x=-3 | x=0");
1.128 if UnparseC.term (or2list t) = "[x = 3, x = - 3, x = 0]" then ()
1.129 else error "HOL.eq ? HOL.disj ? changed";