1.1 --- a/test/Tools/isac/BaseDefinitions/termC.sml Sun Oct 09 06:53:03 2022 +0200
1.2 +++ b/test/Tools/isac/BaseDefinitions/termC.sml Sun Oct 09 07:44:22 2022 +0200
1.3 @@ -186,7 +186,7 @@
1.4 "\<not> ?bdv occurs_in ?a \<Longrightarrow>\n(?a + ?bdv = 0) = (?bdv = - 1 * ?a)"
1.5 then ()
1.6 else error "termC.sml d1_isolate_add2";
1.7 - val subst = [(TermC.str2term "bdv", TermC.str2term "x")];
1.8 + val subst = [(TermC.parse_test @{context} "bdv", TermC.parse_test @{context} "x")];
1.9 val t = (Eval.norm o Thm.prop_of) @{thm d1_isolate_add2};
1.10 val t' = TermC.inst_bdv subst t;
1.11 if UnparseC.term t' = "\<not> x occurs_in ?a \<Longrightarrow> (?a + x = 0) = (x = - 1 * ?a)"
1.12 @@ -199,10 +199,10 @@
1.13 (*default_print_depth 5;*)
1.14
1.15 val subst =
1.16 - [(TermC.str2term "bdv_1", TermC.str2term "c"),
1.17 - (TermC.str2term "bdv_2", TermC.str2term "c_2"),
1.18 - (TermC.str2term "bdv_3", TermC.str2term "c_3"),
1.19 - (TermC.str2term "bdv_4", TermC.str2term "c_4")];
1.20 + [(TermC.parse_test @{context} "bdv_1", TermC.parse_test @{context} "c"),
1.21 + (TermC.parse_test @{context} "bdv_2", TermC.parse_test @{context} "c_2"),
1.22 + (TermC.parse_test @{context} "bdv_3", TermC.parse_test @{context} "c_3"),
1.23 + (TermC.parse_test @{context} "bdv_4", TermC.parse_test @{context} "c_4")];
1.24 val t = (Eval.norm o Thm.prop_of) @{thm separate_bdvs_add};
1.25 val t' = TermC.inst_bdv subst t;
1.26
1.27 @@ -213,9 +213,9 @@
1.28 "----------- subst_atomic_all ---------------------------";
1.29 "----------- subst_atomic_all ---------------------------";
1.30 "----------- subst_atomic_all ---------------------------";
1.31 - val t = TermC.str2term "(tl vs_vs) from vs_vs occur_exactly_in (NTH 1 (es_es::bool list))";
1.32 - val env = [(TermC.str2term "vs_vs::real list", TermC.str2term "[c, c_2]"),
1.33 - (TermC.str2term "es_es::bool list", TermC.str2term "[c_2 = 0, c + c_2 = 1]")];
1.34 + val t = TermC.parse_test @{context} "(tl vs_vs) from vs_vs occur_exactly_in (NTH 1 (es_es::bool list))";
1.35 + val env = [(TermC.parse_test @{context} "vs_vs::real list", TermC.parse_test @{context} "[c, c_2]"),
1.36 + (TermC.parse_test @{context} "es_es::bool list", TermC.parse_test @{context} "[c_2 = 0, c + c_2 = 1]")];
1.37 val (all_Free_subst, t') = TermC.subst_atomic_all env t;
1.38
1.39 if all_Free_subst andalso
1.40 @@ -231,8 +231,8 @@
1.41 "----------- Pattern.match ------------------------------";
1.42 "----------- Pattern.match ------------------------------";
1.43 "----------- Pattern.match ------------------------------";
1.44 - val t = TermC.str2term "3 * x\<up>2 = (1::real)";
1.45 - val pat = (TermC.free2var o TermC.str2term) "a * b\<up>2 = (c::real)";
1.46 + val t = TermC.parse_test @{context} "3 * x\<up>2 = (1::real)";
1.47 + val pat = (TermC.free2var o TermC.parse_test @{context}) "a * b\<up>2 = (c::real)";
1.48 (* ! \<up> \<up> ^^!... necessary for Pattern.match, see Logic.varify_global below*)
1.49 val insts = Pattern.match @{theory "Isac_Knowledge"} (pat, t) (Vartab.empty, Vartab.empty);
1.50 (*default_print_depth 3; 999*) insts;
1.51 @@ -243,7 +243,7 @@
1.52 (("c", 0), ("Real.real", Free ("1", "Real.real")))})*)
1.53
1.54 "----- throws exn MATCH...";
1.55 -(* val t = TermC.str2term "x";
1.56 +(* val t = TermC.parse_test @{context} "x";
1.57 (Pattern.match @{theory "Isac_Knowledge"} (pat, t) (Vartab.empty, Vartab.empty))
1.58 handle MATCH => ???; *)
1.59
1.60 @@ -283,7 +283,7 @@
1.61 else ();
1.62
1.63 "----- test 2: Nok";
1.64 - val pa = Logic.varify_global (TermC.str2term "a = (0::real)");(*<<<<<<<-------------*)
1.65 + val pa = Logic.varify_global (TermC.parse_test @{context} "a = (0::real)");(*<<<<<<<-------------*)
1.66 tracing "paLo2=..."; TermC.atomty pa; tracing "...=paLo2";
1.67 (***
1.68 *** Const (op =, real => real => bool)
1.69 @@ -291,11 +291,11 @@
1.70 *** . Var ((0, 0), real)
1.71 ***)
1.72 "----- test 2a true";
1.73 - val tm = TermC.str2term "-8 - 2 * x + x ^ 2 = (0::real)"; (*<<<<<<<-------------*)
1.74 + val tm = TermC.parse_test @{context} "-8 - 2 * x + x ^ 2 = (0::real)"; (*<<<<<<<-------------*)
1.75 if TermC.matches thy tm pa then ()
1.76 else error "termC.sml diff.behav. in TermC.matches true 2";
1.77 "----- test 2b false";
1.78 - val tm = TermC.str2term "-8 - 2 * x + x ^ 2 = (3::real)"; (*<<<<<<<-------------*)
1.79 + val tm = TermC.parse_test @{context} "-8 - 2 * x + x ^ 2 = (3::real)"; (*<<<<<<<-------------*)
1.80 if TermC.matches thy tm pa then error "termC.sml diff.behav. in TermC.matches false 2"
1.81 else ();
1.82 (* i.e. !!!!!!!!!!!!!!!!! THIS KIND OF PATTERN IS NOT RELIABLE !!!!!!!!!!!!!!!!!
1.83 @@ -303,7 +303,7 @@
1.84 else ();*)
1.85
1.86 "----- test 3: OK";
1.87 - val pa = TermC.free2var (TermC.str2term "a = (0::real)");(*<<<<<<<-------------*)
1.88 + val pa = TermC.free2var (TermC.parse_test @{context} "a = (0::real)");(*<<<<<<<-------------*)
1.89 tracing "paF2=..."; TermC.atomty pa; tracing "...=paF2";
1.90 (***
1.91 *** Const (op =, real => real => bool)
1.92 @@ -311,22 +311,22 @@
1.93 *** . Free (0, real)
1.94 ***)
1.95 "----- test 3a true";
1.96 - val tm = TermC.str2term "-8 - 2 * x + x ^ 2 = (0::real)"; (*<<<<<<<-------------*)
1.97 + val tm = TermC.parse_test @{context} "-8 - 2 * x + x ^ 2 = (0::real)"; (*<<<<<<<-------------*)
1.98 if TermC.matches thy tm pa then ()
1.99 else error "termC.sml diff.behav. in TermC.matches true 3";
1.100 "----- test 3b false";
1.101 - val tm = TermC.str2term "-8 - 2 * x + x ^ 2 = (3::real)"; (*<<<<<<<-------------*)
1.102 + val tm = TermC.parse_test @{context} "-8 - 2 * x + x ^ 2 = (3::real)"; (*<<<<<<<-------------*)
1.103 if TermC.matches thy tm pa then error "termC.sml diff.behav. in TermC.matches false 3"
1.104 else ();
1.105
1.106 "----- test 4=3 with specific data";
1.107 - val pa = TermC.free2var (TermC.str2term "M_b 0");
1.108 + val pa = TermC.free2var (TermC.parse_test @{context} "M_b 0");
1.109 "----- test 4a true";
1.110 - val tm = TermC.str2term "M_b 0";
1.111 + val tm = TermC.parse_test @{context} "M_b 0";
1.112 if TermC.matches thy tm pa then ()
1.113 else error "termC.sml diff.behav. in TermC.matches true 4";
1.114 "----- test 4b false";
1.115 - val tm = TermC.str2term "M_b x";
1.116 + val tm = TermC.parse_test @{context} "M_b x";
1.117 if TermC.matches thy tm pa then error "termC.sml diff.behav. in TermC.matches false 4"
1.118 else ();
1.119
1.120 @@ -537,10 +537,10 @@
1.121 "----------- fun TermC.is_bdv_subst ------------------------------------------------------------------";
1.122 "----------- fun TermC.is_bdv_subst ------------------------------------------------------------------";
1.123 "----------- fun TermC.is_bdv_subst ------------------------------------------------------------------";
1.124 -if TermC.is_bdv_subst (TermC.str2term "[(''bdv'', v_v)]") then ()
1.125 +if TermC.is_bdv_subst (TermC.parse_test @{context} "[(''bdv'', v_v)]") then ()
1.126 else error "TermC.is_bdv_subst canged 1";
1.127
1.128 -if TermC.is_bdv_subst (TermC.str2term "[(''bdv_1'', v_s1),(''bdv_2'', v_s2)]") then ()
1.129 +if TermC.is_bdv_subst (TermC.parse_test @{context} "[(''bdv_1'', v_s1),(''bdv_2'', v_s2)]") then ()
1.130 else error "TermC.is_bdv_subst canged 2";
1.131
1.132 "----------- fun str_of_int --------------------------------------------------------------------";
1.133 @@ -581,41 +581,41 @@
1.134 case ThmC_Def.int_opt_of_string "-123" of
1.135 SOME ~123 => () | _ => raise error "ThmC_Def.int_opt_of_string -123 changed";
1.136
1.137 -val t = TermC.str2term "1";
1.138 +val t = TermC.parse_test @{context} "1";
1.139 if TermC.is_num t = true then () else error "TermC.is_num 1";
1.140
1.141 -val t = TermC.str2term "-1";
1.142 +val t = TermC.parse_test @{context} "-1";
1.143 if TermC.is_num t = true then () else error "TermC.is_num -1";
1.144
1.145 -val t = TermC.str2term "a123";
1.146 +val t = TermC.parse_test @{context} "a123";
1.147 if TermC.is_num t = false then () else error "TermC.is_num a123";
1.148
1.149 "----------- fun TermC.is_f_x ------------------------------------------------------------------------";
1.150 "----------- fun TermC.is_f_x ------------------------------------------------------------------------";
1.151 "----------- fun TermC.is_f_x ------------------------------------------------------------------------";
1.152 -val t = TermC.str2term "q_0/2 * L * x";
1.153 +val t = TermC.parse_test @{context} "q_0/2 * L * x";
1.154 if TermC.is_f_x t = false then () else error "TermC.is_f_x q_0/2 * L * x";
1.155
1.156 -val t = TermC.str2term "M_b x";
1.157 +val t = TermC.parse_test @{context} "M_b x";
1.158 if TermC.is_f_x t = true then () else error "M_b x";
1.159
1.160 "----------- fun list2isalist, fun isalist2list ------------------------------------------------";
1.161 "----------- fun list2isalist, fun isalist2list ------------------------------------------------";
1.162 "----------- fun list2isalist, fun isalist2list ------------------------------------------------";
1.163 -val t = TermC.str2term "R=(R::real)";
1.164 +val t = TermC.parse_test @{context} "R=(R::real)";
1.165 val T = type_of t;
1.166 val ss = TermC.list2isalist T [t,t,t];
1.167 if UnparseC.term ss = "[R = R, R = R, R = R]" then () else error "list2isalist 1";
1.168
1.169 -val t = TermC.str2term "[a=b,c=d,e=f]";
1.170 +val t = TermC.parse_test @{context} "[a=b,c=d,e=f]";
1.171 val il = TermC.isalist2list t;
1.172 if UnparseC.terms il = "[\"a = b\", \"c = d\", \"e = f\"]" then () else error "isalist2list 2";
1.173
1.174 -val t = TermC.str2term "[a=b,c=d,e=f]";
1.175 +val t = TermC.parse_test @{context} "[a=b,c=d,e=f]";
1.176 val il = TermC.isalist2list t;
1.177 if UnparseC.terms il = "[\"a = b\", \"c = d\", \"e = f\"]" then () else error "isalist2list 3";
1.178
1.179 -val t = TermC.str2term "ss___s::bool list";
1.180 +val t = TermC.parse_test @{context} "ss___s::bool list";
1.181 (TermC.isalist2list t; error "isalist2list 1") handle TERM ("isalist2list applied to NON-list: ", _) =>();
1.182
1.183 "----------- fun TermC.strip_imp_prems', fun TermC.ins_concl -----------------------------------------------";
1.184 @@ -647,7 +647,7 @@
1.185 val t = TermC.mk_factroot "SqRoot.sqrt" T 2 3;
1.186 if UnparseC.term t = "2 * ??.SqRoot.sqrt 3" then () else error "mk_factroot";
1.187
1.188 -val t = TermC.str2term "aaa + bbb";
1.189 +val t = TermC.parse_test @{context} "aaa + bbb";
1.190 val op_ as Const (\<^const_name>\<open>plus\<close>, Top) $ Free ("aaa", T1) $ Free ("bbb", T2) = t;
1.191 val t' = TermC.mk_num_op_num T1 T2 (\<^const_name>\<open>plus\<close>, Top) 2 3;
1.192 if UnparseC.term t' = "2 + 3" then () else error "mk_num_op_num";
1.193 @@ -664,11 +664,11 @@
1.194 "----------- fun TermC.is_list -----------------------------------------------------------------------";
1.195 "----------- fun TermC.is_list -----------------------------------------------------------------------";
1.196 val (SOME ct) = TermC.parseNEW ctxt "lll::real list";
1.197 -val t = TermC.str2term "lll::real list";
1.198 +val t = TermC.parse_test @{context} "lll::real list";
1.199 val ty = Term.type_of ct;
1.200 if TermC.is_list t = false then () else error "TermC.is_list lll::real list";
1.201
1.202 -val t = TermC.str2term "[a, b, c]";
1.203 +val t = TermC.parse_test @{context} "[a, b, c]";
1.204 val ty = Term.type_of ct;
1.205 if TermC.is_list t = true then () else error "TermC.is_list [a, b, c]";
1.206