1.1 --- a/test/Tools/isac/BaseDefinitions/termC.sml Sun Jan 29 14:31:56 2023 +0100
1.2 +++ b/test/Tools/isac/BaseDefinitions/termC.sml Mon Jan 30 09:47:18 2023 +0100
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.parse_test @{context} "bdv", TermC.parse_test @{context} "x")];
1.8 + val subst = [(ParseC.parse_test @{context} "bdv", ParseC.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.parse_test @{context} "bdv_1", TermC.parse_test @{context} "c"),
1.17 - (TermC.parse_test @{context} "bdv_2", TermC.parse_test @{context} "c_2"),
1.18 - (TermC.parse_test @{context} "bdv_3", TermC.parse_test @{context} "c_3"),
1.19 - (TermC.parse_test @{context} "bdv_4", TermC.parse_test @{context} "c_4")];
1.20 + [(ParseC.parse_test @{context} "bdv_1", ParseC.parse_test @{context} "c"),
1.21 + (ParseC.parse_test @{context} "bdv_2", ParseC.parse_test @{context} "c_2"),
1.22 + (ParseC.parse_test @{context} "bdv_3", ParseC.parse_test @{context} "c_3"),
1.23 + (ParseC.parse_test @{context} "bdv_4", ParseC.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.parse_test @{context} "(tl vs_vs) from vs_vs occur_exactly_in (NTH 1 (es_es::bool list))";
1.32 - val env = [(TermC.parse_test @{context} "vs_vs::real list", TermC.parse_test @{context} "[c, c_2]"),
1.33 - (TermC.parse_test @{context} "es_es::bool list", TermC.parse_test @{context} "[c_2 = 0, c + c_2 = 1]")];
1.34 + val t = ParseC.parse_test @{context} "(tl vs_vs) from vs_vs occur_exactly_in (NTH 1 (es_es::bool list))";
1.35 + val env = [(ParseC.parse_test @{context} "vs_vs::real list", ParseC.parse_test @{context} "[c, c_2]"),
1.36 + (ParseC.parse_test @{context} "es_es::bool list", ParseC.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.parse_test @{context} "3 * x\<up>2 = (1::real)";
1.45 - val pat = (TermC.mk_Var o TermC.parse_test @{context}) "a * b\<up>2 = (c::real)";
1.46 + val t = ParseC.parse_test @{context} "3 * x\<up>2 = (1::real)";
1.47 + val pat = (TermC.mk_Var o ParseC.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.parse_test @{context} "x";
1.56 +(* val t = ParseC.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.parse_test @{context} "a = (0::real)");(*<<<<<<<-------------*)
1.65 + val pa = Logic.varify_global (ParseC.parse_test @{context} "a = (0::real)");(*<<<<<<<-------------*)
1.66 tracing "paLo2=..."; TermC.atom_trace_detail @{context} 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.parse_test @{context} "-8 - 2 * x + x ^ 2 = (0::real)"; (*<<<<<<<-------------*)
1.74 + val tm = ParseC.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.parse_test @{context} "-8 - 2 * x + x ^ 2 = (3::real)"; (*<<<<<<<-------------*)
1.79 + val tm = ParseC.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.mk_Var (TermC.parse_test @{context} "a = (0::real)");(*<<<<<<<-------------*)
1.88 + val pa = TermC.mk_Var (ParseC.parse_test @{context} "a = (0::real)");(*<<<<<<<-------------*)
1.89 tracing "paF2=..."; TermC.atom_trace_detail @{context} 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.parse_test @{context} "-8 - 2 * x + x ^ 2 = (0::real)"; (*<<<<<<<-------------*)
1.97 + val tm = ParseC.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.parse_test @{context} "-8 - 2 * x + x ^ 2 = (3::real)"; (*<<<<<<<-------------*)
1.102 + val tm = ParseC.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.mk_Var (TermC.parse_test @{context} "M_b 0");
1.108 + val pa = TermC.mk_Var (ParseC.parse_test @{context} "M_b 0");
1.109 "----- test 4a true";
1.110 - val tm = TermC.parse_test @{context} "M_b 0";
1.111 + val tm = ParseC.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.parse_test @{context} "M_b x";
1.116 + val tm = ParseC.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 @@ -362,7 +362,7 @@
1.121 val ctxt = @{context}
1.122 val str = "x + 2*z";
1.123 val t = Syntax.read_term_global thy str;
1.124 - val t = Model_Pattern.adapt_term_to_type ctxt (Syntax.read_term_global thy str);
1.125 + val t = ParseC.adapt_term_to_type ctxt (Syntax.read_term_global thy str);
1.126 Thm.global_cterm_of thy t;
1.127 case TermC.parseNEW ctxt str of
1.128 SOME t' => t'
1.129 @@ -450,7 +450,7 @@
1.130 "----- read_term_pattern ---";
1.131 val t = (thy, str) |>> Proof_Context.init_global
1.132 |-> Proof_Context.read_term_pattern;
1.133 -val t_real = Model_Pattern.adapt_term_to_type ctxt t;
1.134 +val t_real = ParseC.adapt_term_to_type ctxt t;
1.135 if UnparseC.term_in_ctxt ctxt t_real =
1.136 "\<not> (matchsub ((?a::real) + ((?b::real) + (?c::real))) (t_t::real) \<or>\n "
1.137 ^ "matchsub (?a + (?b - ?c)) t_t \<or>\n "
1.138 @@ -540,10 +540,10 @@
1.139 "----------- fun TermC.is_bdv_subst ------------------------------------------------------------------";
1.140 "----------- fun TermC.is_bdv_subst ------------------------------------------------------------------";
1.141 "----------- fun TermC.is_bdv_subst ------------------------------------------------------------------";
1.142 -if TermC.is_bdv_subst (TermC.parse_test @{context} "[(''bdv'', v_v)]") then ()
1.143 +if TermC.is_bdv_subst (ParseC.parse_test @{context} "[(''bdv'', v_v)]") then ()
1.144 else error "TermC.is_bdv_subst canged 1";
1.145
1.146 -if TermC.is_bdv_subst (TermC.parse_test @{context} "[(''bdv_1'', v_s1),(''bdv_2'', v_s2)]") then ()
1.147 +if TermC.is_bdv_subst (ParseC.parse_test @{context} "[(''bdv_1'', v_s1),(''bdv_2'', v_s2)]") then ()
1.148 else error "TermC.is_bdv_subst canged 2";
1.149
1.150 "----------- fun str_of_int --------------------------------------------------------------------";
1.151 @@ -584,41 +584,41 @@
1.152 case ThmC_Def.int_opt_of_string "-123" of
1.153 SOME ~123 => () | _ => raise error "ThmC_Def.int_opt_of_string -123 changed";
1.154
1.155 -val t = TermC.parse_test @{context} "1";
1.156 +val t = ParseC.parse_test @{context} "1";
1.157 if TermC.is_num t = true then () else error "TermC.is_num 1";
1.158
1.159 -val t = TermC.parse_test @{context} "-1";
1.160 +val t = ParseC.parse_test @{context} "-1";
1.161 if TermC.is_num t = true then () else error "TermC.is_num -1";
1.162
1.163 -val t = TermC.parse_test @{context} "a123";
1.164 +val t = ParseC.parse_test @{context} "a123";
1.165 if TermC.is_num t = false then () else error "TermC.is_num a123";
1.166
1.167 "----------- fun TermC.is_f_x ------------------------------------------------------------------------";
1.168 "----------- fun TermC.is_f_x ------------------------------------------------------------------------";
1.169 "----------- fun TermC.is_f_x ------------------------------------------------------------------------";
1.170 -val t = TermC.parse_test @{context} "q_0/2 * L * x";
1.171 +val t = ParseC.parse_test @{context} "q_0/2 * L * x";
1.172 if TermC.is_f_x t = false then () else error "TermC.is_f_x q_0/2 * L * x";
1.173
1.174 -val t = TermC.parse_test @{context} "M_b x";
1.175 +val t = ParseC.parse_test @{context} "M_b x";
1.176 if TermC.is_f_x t = true then () else error "M_b x";
1.177
1.178 "----------- fun list2isalist, fun isalist2list ------------------------------------------------";
1.179 "----------- fun list2isalist, fun isalist2list ------------------------------------------------";
1.180 "----------- fun list2isalist, fun isalist2list ------------------------------------------------";
1.181 -val t = TermC.parse_test @{context} "R=(R::real)";
1.182 +val t = ParseC.parse_test @{context} "R=(R::real)";
1.183 val T = type_of t;
1.184 val ss = TermC.list2isalist T [t,t,t];
1.185 if UnparseC.term ss = "[R = R, R = R, R = R]" then () else error "list2isalist 1";
1.186
1.187 -val t = TermC.parse_test @{context} "[a=b,c=d,e=f]";
1.188 +val t = ParseC.parse_test @{context} "[a=b,c=d,e=f]";
1.189 val il = TermC.isalist2list t;
1.190 if UnparseC.terms il = "[\"a = b\", \"c = d\", \"e = f\"]" then () else error "isalist2list 2";
1.191
1.192 -val t = TermC.parse_test @{context} "[a=b,c=d,e=f]";
1.193 +val t = ParseC.parse_test @{context} "[a=b,c=d,e=f]";
1.194 val il = TermC.isalist2list t;
1.195 if UnparseC.terms il = "[\"a = b\", \"c = d\", \"e = f\"]" then () else error "isalist2list 3";
1.196
1.197 -val t = TermC.parse_test @{context} "ss___s::bool list";
1.198 +val t = ParseC.parse_test @{context} "ss___s::bool list";
1.199 (TermC.isalist2list t; error "isalist2list 1") handle TERM ("isalist2list applied to NON-list: ", _) =>();
1.200
1.201 "----------- fun TermC.strip_imp_prems', fun TermC.ins_concl -----------------------------------------------";
1.202 @@ -650,7 +650,7 @@
1.203 val t = TermC.mk_factroot "SqRoot.sqrt" T 2 3;
1.204 if UnparseC.term t = "2 * ??.SqRoot.sqrt 3" then () else error "mk_factroot";
1.205
1.206 -val t = TermC.parse_test @{context} "aaa + bbb";
1.207 +val t = ParseC.parse_test @{context} "aaa + bbb";
1.208 val op_ as Const (\<^const_name>\<open>plus\<close>, Top) $ Free ("aaa", T1) $ Free ("bbb", T2) = t;
1.209 val t' = TermC.mk_num_op_num T1 T2 (\<^const_name>\<open>plus\<close>, Top) 2 3;
1.210 if UnparseC.term t' = "2 + 3" then () else error "mk_num_op_num";
1.211 @@ -667,11 +667,11 @@
1.212 "----------- fun TermC.is_list -----------------------------------------------------------------------";
1.213 "----------- fun TermC.is_list -----------------------------------------------------------------------";
1.214 val (SOME ct) = TermC.parseNEW ctxt "lll::real list";
1.215 -val t = TermC.parse_test @{context} "lll::real list";
1.216 +val t = ParseC.parse_test @{context} "lll::real list";
1.217 val ty = Term.type_of ct;
1.218 if TermC.is_list t = false then () else error "TermC.is_list lll::real list";
1.219
1.220 -val t = TermC.parse_test @{context} "[a, b, c]";
1.221 +val t = ParseC.parse_test @{context} "[a, b, c]";
1.222 val ty = Term.type_of ct;
1.223 if TermC.is_list t = true then () else error "TermC.is_list [a, b, c]";
1.224