wneuper/isa: comparison test/Tools/isac/BaseDefinitions/termC.sml

equal deleted inserted replaced

-:873f40b097bb
+:c4b24621077e
 "----------- inst_bdv -----------------------------------";
 if (UnparseC.term o Thm.prop_of) @{thm d1_isolate_add2} =
 "\<not> ?bdv occurs_in ?a \<Longrightarrow>\n(?a + ?bdv = 0) = (?bdv = - 1 * ?a)"
 then ()
 else error "termC.sml d1_isolate_add2";
-val subst = [(TermC.parse_test @{context} "bdv", TermC.parse_test @{context} "x")];
+val subst = [(ParseC.parse_test @{context} "bdv", ParseC.parse_test @{context} "x")];
 val t = (Eval.norm o Thm.prop_of)  @{thm d1_isolate_add2};
 val t' = TermC.inst_bdv subst t;
 if UnparseC.term t' = "\<not> x occurs_in ?a \<Longrightarrow> (?a + x = 0) = (x = - 1 * ?a)"
 then ()
 else error "termC.sml inst_bdv 1";
 "?bdv_4.0] occur_exactly_in ?a \<Longrightarrow>\n(?a + ?b = ?c) = (?b = ?c + - (1::?'a) * ?a)"
 then () else error "termC.sml separate_bdvs_add";
 (*default_print_depth 5;*)
 val subst =
-[(TermC.parse_test @{context} "bdv_1", TermC.parse_test @{context} "c"),
+[(ParseC.parse_test @{context} "bdv_1", ParseC.parse_test @{context} "c"),
-	   (TermC.parse_test @{context} "bdv_2", TermC.parse_test @{context} "c_2"),
+	   (ParseC.parse_test @{context} "bdv_2", ParseC.parse_test @{context} "c_2"),
-	   (TermC.parse_test @{context} "bdv_3", TermC.parse_test @{context} "c_3"),
+	   (ParseC.parse_test @{context} "bdv_3", ParseC.parse_test @{context} "c_3"),
-	   (TermC.parse_test @{context} "bdv_4", TermC.parse_test @{context} "c_4")];
+	   (ParseC.parse_test @{context} "bdv_4", ParseC.parse_test @{context} "c_4")];
 val t = (Eval.norm o Thm.prop_of)  @{thm separate_bdvs_add};
 val t' = TermC.inst_bdv subst t;
 if UnparseC.term t' = "[] from [c, c_2, c_3, c_4] occur_exactly_in ?a \<Longrightarrow>\n" ^
 "(?a + ?b = ?c) = (?b = ?c + - (1::?'a) * ?a)"
 then () else error "termC.sml inst_bdv 2";
 "----------- subst_atomic_all ---------------------------";
 "----------- subst_atomic_all ---------------------------";
 "----------- subst_atomic_all ---------------------------";
-val t = TermC.parse_test @{context} "(tl vs_vs) from vs_vs occur_exactly_in (NTH 1 (es_es::bool list))";
+val t = ParseC.parse_test @{context} "(tl vs_vs) from vs_vs occur_exactly_in (NTH 1 (es_es::bool list))";
-val env = [(TermC.parse_test @{context} "vs_vs::real list", TermC.parse_test @{context} "[c, c_2]"),
+val env = [(ParseC.parse_test @{context} "vs_vs::real list", ParseC.parse_test @{context} "[c, c_2]"),
-	   (TermC.parse_test @{context} "es_es::bool list", TermC.parse_test @{context} "[c_2 = 0, c + c_2 = 1]")];
+	   (ParseC.parse_test @{context} "es_es::bool list", ParseC.parse_test @{context} "[c_2 = 0, c + c_2 = 1]")];
 val (all_Free_subst, t') = TermC.subst_atomic_all env t;
 if all_Free_subst andalso
 UnparseC.term t' = "tl [c, c_2] from [c, c_2] occur_exactly_in NTH 1 [c_2 = 0, c + c_2 = 1]"
 then ()
 else error "TermC.subst_atomic_all should be 'false'";
 "----------- Pattern.match ------------------------------";
 "----------- Pattern.match ------------------------------";
 "----------- Pattern.match ------------------------------";
-val t = TermC.parse_test @{context} "3 * x\<up>2 = (1::real)";
+val t = ParseC.parse_test @{context} "3 * x\<up>2 = (1::real)";
-val pat = (TermC.mk_Var o TermC.parse_test @{context}) "a * b\<up>2 = (c::real)";
+val pat = (TermC.mk_Var o ParseC.parse_test @{context}) "a * b\<up>2 = (c::real)";
 (*        ! \<up>  \<up> ^^!... necessary for Pattern.match, see Logic.varify_global below*)
 val insts = Pattern.match @{theory "Isac_Knowledge"} (pat, t) (Vartab.empty, Vartab.empty);
 (*default_print_depth 3; 999*) insts;
 (*val insts =
 ({},
 {(("a", 0), ("Real.real", Free ("3", "Real.real"))),
 (("b", 0), ("Real.real", Free ("x", "Real.real"))),
 (("c", 0), ("Real.real", Free ("1", "Real.real")))})*)
 "----- throws exn MATCH...";
-(* val t = TermC.parse_test @{context} "x";
+(* val t = ParseC.parse_test @{context} "x";
 (Pattern.match @{theory "Isac_Knowledge"} (pat, t) (Vartab.empty, Vartab.empty))
 handle MATCH => ???; *)
 val thy = @{theory "Complex_Main"};
 val PARSE = Syntax.read_term_global thy;
 val tm = @{term "-8 - 2 * x + x ^ 2 = (3::real)"};    (*<<<<<<<---------------*)
 if TermC.matches thy tm pa then error "termC.sml diff.behav. in TermC.matches false 1"
 else ();
 "----- test 2: Nok";
-val pa = Logic.varify_global (TermC.parse_test @{context} "a = (0::real)");(*<<<<<<<-------------*)
+val pa = Logic.varify_global (ParseC.parse_test @{context} "a = (0::real)");(*<<<<<<<-------------*)
 tracing "paLo2=..."; TermC.atom_trace_detail @{context} pa; tracing "...=paLo2";
 (***
 *** Const (op =, real => real => bool)
 *** . Var ((a, 0), real)
 *** . Var ((0, 0), real)
 ***)
 "----- test 2a true";
-val tm = TermC.parse_test @{context} "-8 - 2 * x + x ^ 2 = (0::real)";     (*<<<<<<<-------------*)
+val tm = ParseC.parse_test @{context} "-8 - 2 * x + x ^ 2 = (0::real)";     (*<<<<<<<-------------*)
 if TermC.matches thy tm pa then ()
 else error "termC.sml diff.behav. in TermC.matches true 2";
 "----- test 2b false";
-val tm = TermC.parse_test @{context} "-8 - 2 * x + x ^ 2 = (3::real)";     (*<<<<<<<-------------*)
+val tm = ParseC.parse_test @{context} "-8 - 2 * x + x ^ 2 = (3::real)";     (*<<<<<<<-------------*)
 if TermC.matches thy tm pa then error "termC.sml diff.behav. in TermC.matches false 2"
 else ();
 (* i.e. !!!!!!!!!!!!!!!!! THIS KIND OF PATTERN IS NOT RELIABLE !!!!!!!!!!!!!!!!!
 if TermC.matches thy tm pa then error "termC.sml diff.behav. in TermC.matches false 2"
 else ();*)
 "----- test 3: OK";
-val pa = TermC.mk_Var (TermC.parse_test @{context} "a = (0::real)");(*<<<<<<<-------------*)
+val pa = TermC.mk_Var (ParseC.parse_test @{context} "a = (0::real)");(*<<<<<<<-------------*)
 tracing "paF2=..."; TermC.atom_trace_detail @{context} pa; tracing "...=paF2";
 (***
 *** Const (op =, real => real => bool)
 *** . Var ((a, 0), real)
 *** . Free (0, real)
 ***)
 "----- test 3a true";
-val tm = TermC.parse_test @{context} "-8 - 2 * x + x ^ 2 = (0::real)";     (*<<<<<<<-------------*)
+val tm = ParseC.parse_test @{context} "-8 - 2 * x + x ^ 2 = (0::real)";     (*<<<<<<<-------------*)
 if TermC.matches thy tm pa then ()
 else error "termC.sml diff.behav. in TermC.matches true 3";
 "----- test 3b false";
-val tm = TermC.parse_test @{context} "-8 - 2 * x + x ^ 2 = (3::real)";     (*<<<<<<<-------------*)
+val tm = ParseC.parse_test @{context} "-8 - 2 * x + x ^ 2 = (3::real)";     (*<<<<<<<-------------*)
 if TermC.matches thy tm pa then error "termC.sml diff.behav. in TermC.matches false 3"
 else ();
 "----- test 4=3 with specific data";
-val pa = TermC.mk_Var (TermC.parse_test @{context} "M_b 0");
+val pa = TermC.mk_Var (ParseC.parse_test @{context} "M_b 0");
 "----- test 4a true";
-val tm = TermC.parse_test @{context} "M_b 0";
+val tm = ParseC.parse_test @{context} "M_b 0";
 if TermC.matches thy tm pa then ()
 else error "termC.sml diff.behav. in TermC.matches true 4";
 "----- test 4b false";
-val tm = TermC.parse_test @{context} "M_b x";
+val tm = ParseC.parse_test @{context} "M_b x";
 if TermC.matches thy tm pa then error "termC.sml diff.behav. in TermC.matches false 4"
 else ();
 "----------- fun TermC.parse, fun TermC.parse_patt, fun T_a2real -------------------------------";
 "----------- fun TermC.parse, fun TermC.parse_patt, fun T_a2real -------------------------------";
 "---------------";
 val ctxt = @{context}
 val str = "x + 2*z";
 val t =  Syntax.read_term_global thy str;
-val t = Model_Pattern.adapt_term_to_type ctxt (Syntax.read_term_global thy str);
+val t = ParseC.adapt_term_to_type ctxt (Syntax.read_term_global thy str);
 Thm.global_cterm_of thy t;
 case TermC.parseNEW ctxt str of
 SOME t' => t'
 | NONE => error "termC.sml parsing 'x + 2*z' failed";
 val ctxt = Proof_Context.init_global thy;
 val ctxt = Config.put show_types true ctxt;
 "----- read_term_pattern ---";
 val t = (thy, str) |>> Proof_Context.init_global
 |-> Proof_Context.read_term_pattern;
-val t_real = Model_Pattern.adapt_term_to_type ctxt t;
+val t_real = ParseC.adapt_term_to_type ctxt t;
 if UnparseC.term_in_ctxt ctxt t_real =
 "\<not> (matchsub ((?a::real) + ((?b::real) + (?c::real))) (t_t::real) \<or>\n        "
 ^ "matchsub (?a + (?b - ?c)) t_t \<or>\n        "
 ^ "matchsub (?a - (?b + ?c)) t_t \<or> matchsub (?a + (?b - ?c)) t_t)" then ()
 else error "matchsub";
 *)
 "----------- fun TermC.is_bdv_subst ------------------------------------------------------------------";
 "----------- fun TermC.is_bdv_subst ------------------------------------------------------------------";
 "----------- fun TermC.is_bdv_subst ------------------------------------------------------------------";
-if TermC.is_bdv_subst (TermC.parse_test @{context} "[(''bdv'', v_v)]") then ()
+if TermC.is_bdv_subst (ParseC.parse_test @{context} "[(''bdv'', v_v)]") then ()
 else error "TermC.is_bdv_subst canged 1";
-if TermC.is_bdv_subst (TermC.parse_test @{context} "[(''bdv_1'', v_s1),(''bdv_2'', v_s2)]") then ()
+if TermC.is_bdv_subst (ParseC.parse_test @{context} "[(''bdv_1'', v_s1),(''bdv_2'', v_s2)]") then ()
 else error "TermC.is_bdv_subst canged 2";
 "----------- fun str_of_int --------------------------------------------------------------------";
 "----------- fun str_of_int --------------------------------------------------------------------";
 "----------- fun str_of_int --------------------------------------------------------------------";
 case ThmC_Def.int_opt_of_string "#123" of
 NONE => () | _ => raise error "ThmC_Def.int_opt_of_string  #123  changed";
 case ThmC_Def.int_opt_of_string "-123" of
 SOME ~123 => () | _ => raise error "ThmC_Def.int_opt_of_string  -123  changed";
-val t = TermC.parse_test @{context} "1";
+val t = ParseC.parse_test @{context} "1";
 if TermC.is_num t = true then () else error "TermC.is_num   1";
-val t = TermC.parse_test @{context} "-1";
+val t = ParseC.parse_test @{context} "-1";
 if TermC.is_num t = true then () else error "TermC.is_num  -1";
-val t = TermC.parse_test @{context} "a123";
+val t = ParseC.parse_test @{context} "a123";
 if TermC.is_num t = false then () else error "TermC.is_num   a123";
 "----------- fun TermC.is_f_x ------------------------------------------------------------------------";
 "----------- fun TermC.is_f_x ------------------------------------------------------------------------";
 "----------- fun TermC.is_f_x ------------------------------------------------------------------------";
-val t = TermC.parse_test @{context} "q_0/2 * L * x";
+val t = ParseC.parse_test @{context} "q_0/2 * L * x";
 if TermC.is_f_x t = false then () else error "TermC.is_f_x   q_0/2 * L * x";
-val t = TermC.parse_test @{context} "M_b x";
+val t = ParseC.parse_test @{context} "M_b x";
 if TermC.is_f_x t = true then () else error "M_b x";
 "----------- fun list2isalist, fun isalist2list ------------------------------------------------";
 "----------- fun list2isalist, fun isalist2list ------------------------------------------------";
 "----------- fun list2isalist, fun isalist2list ------------------------------------------------";
-val t = TermC.parse_test @{context} "R=(R::real)";
+val t = ParseC.parse_test @{context} "R=(R::real)";
 val T = type_of t;
 val ss = TermC.list2isalist T [t,t,t];
 if UnparseC.term ss = "[R = R, R = R, R = R]" then () else error "list2isalist 1";
-val t = TermC.parse_test @{context} "[a=b,c=d,e=f]";
+val t = ParseC.parse_test @{context} "[a=b,c=d,e=f]";
 val il = TermC.isalist2list t;
 if UnparseC.terms il = "[\"a = b\", \"c = d\", \"e = f\"]" then () else error "isalist2list 2";
-val t = TermC.parse_test @{context} "[a=b,c=d,e=f]";
+val t = ParseC.parse_test @{context} "[a=b,c=d,e=f]";
 val il = TermC.isalist2list t;
 if UnparseC.terms il = "[\"a = b\", \"c = d\", \"e = f\"]" then () else error "isalist2list 3";
-val t = TermC.parse_test @{context} "ss___s::bool list";
+val t = ParseC.parse_test @{context} "ss___s::bool list";
 (TermC.isalist2list t; error "isalist2list 1") handle TERM ("isalist2list applied to NON-list: ", _) =>();
 "----------- fun TermC.strip_imp_prems', fun TermC.ins_concl -----------------------------------------------";
 "----------- fun TermC.strip_imp_prems', fun TermC.ins_concl -----------------------------------------------";
 "----------- fun TermC.strip_imp_prems', fun TermC.ins_concl -----------------------------------------------";
 "----------- fun mk_factroot, fun mk_num_op_num, -----------------------------------------------";
 val T =  type_of (TermC.parseNEW' ctxt "12::real");
 val t = TermC.mk_factroot "SqRoot.sqrt" T 2 3;
 if UnparseC.term t = "2 * ??.SqRoot.sqrt 3" then () else error "mk_factroot";
-val t = TermC.parse_test @{context} "aaa + bbb";
+val t = ParseC.parse_test @{context} "aaa + bbb";
 val op_ as Const (\<^const_name>\<open>plus\<close>, Top) $ Free ("aaa", T1) $ Free ("bbb", T2) = t;
 val t' = TermC.mk_num_op_num T1 T2 (\<^const_name>\<open>plus\<close>, Top) 2 3;
 if UnparseC.term t' = "2 + 3" then () else error "mk_num_op_num";
 "----------- fun TermC.dest_binop_typ ----------------------------------------------------------------";
 "----------- fun TermC.is_list -----------------------------------------------------------------------";
 "----------- fun TermC.is_list -----------------------------------------------------------------------";
 "----------- fun TermC.is_list -----------------------------------------------------------------------";
 val (SOME ct) = TermC.parseNEW ctxt "lll::real list";
-val t = TermC.parse_test @{context} "lll::real list";
+val t = ParseC.parse_test @{context} "lll::real list";
 val ty = Term.type_of ct;
 if TermC.is_list t = false then () else error "TermC.is_list   lll::real list";
-val t = TermC.parse_test @{context} "[a, b, c]";
+val t = ParseC.parse_test @{context} "[a, b, c]";
 val ty = Term.type_of ct;
 if TermC.is_list t = true then () else error "TermC.is_list  [a, b, c]";
 "----------- fun mk_frac, proper term with uminus ----------------------------------------------";
 "----------- fun mk_frac, proper term with uminus ----------------------------------------------";

changeset 60660	c4b24621077e
parent 60650	06ec8abfd3bc
child 60662	ba258eeb0826