1 (* Title: tests on ProgLang/termC.sml
2 Author: Walther Neuper 051006,
3 (c) due to copyright terms
5 "--------------------------------------------------------";
6 "table of contents --------------------------------------";
7 "--------------------------------------------------------";
8 "----------- inst_bdv -----------------------------------";
9 "----------- subst_atomic_all ---------------------------";
10 "----------- Pattern.match ------------------------------";
11 "----------- fun matches --------------------------------";
12 "------------parse---------------------------------------";
13 "----------- uminus_to_string ---------------------------";
14 "--------------------------------------------------------";
15 "--------------------------------------------------------";
18 (*===== inhibit exn ============================================================
19 "----------- inst_bdv -----------------------------------";
20 "----------- inst_bdv -----------------------------------";
21 "----------- inst_bdv -----------------------------------";
22 if (term2str o prop_of o num_str) @{thm d1_isolate_add2} =
23 "~ ?bdv occurs_in ?a ==> (?a + ?bdv = 0) = (?bdv = -1 * ?a)" then ()
24 else error "termC.sml d1_isolate_add2";
25 val subst = [(str2term "bdv", str2term "x")];
26 val t = (norm o #prop o rep_thm) (num_str @{thm d1_isolate_add2});
27 val t' = inst_bdv subst t;
28 if term2str t' = "~ x occurs_in ?a ==> (?a + x = 0) = (x = -1 * ?a)" then ()
29 else error "termC.sml inst_bdv 1";
31 if string_of_thm (num_str @{thm separate_bdvs_add}) =
32 "\"[] from_ [?bdv_1.0, ?bdv_2.0, ?bdv_3.0, ?bdv_4.0] occur_exactly_in ?a\n\
33 \ ==> (?a + ?b = ?c) = (?b = ?c + -1 * ?a)\"" then ()
34 else error "termC.sml separate_bdvs_add";
35 val subst = [(str2term"bdv_1",str2term"c"),
36 (str2term"bdv_2",str2term"c_2"),
37 (str2term"bdv_3",str2term"c_3"),
38 (str2term"bdv_4",str2term"c_4")];
39 val t = (norm o #prop o rep_thm) (num_str @{thm separate_bdvs_add});
40 val t' = inst_bdv subst t;
41 if term2str t' = "[] from_ [c, c_2, c_3, c_4] occur_exactly_in ?a\n\
42 \==> (?a + ?b = ?c) = (?b = ?c + -1 * ?a)" then ()
43 else error "termC.sml inst_bdv 2";
46 "----------- subst_atomic_all ---------------------------";
47 "----------- subst_atomic_all ---------------------------";
48 "----------- subst_atomic_all ---------------------------";
49 val t = str2term "(tl vs_) from_ vs_ occur_exactly_in (nth_ 1(es_::bool list))";
50 val env = [(str2term"vs_::real list",str2term"[c, c_2]"),
51 (str2term"es_::bool list",str2term"[c_2=0, c+c_2=1]")];
52 val (all_Free_subst, t') = subst_atomic_all env t;
53 if all_Free_subst andalso
54 term2str t' = "tl [c, c_2] from_ [c, c_2] occur_exactly_in nth_ 1 [c_2 = 0, c + c_2 = 1]" then ()
55 else error "termC.sml subst_atomic_all should be 'true'";
58 val (all_Free_subst, t') = subst_atomic_all (tl env) t;
59 if not all_Free_subst andalso
60 term2str t' = "tl vs_ from_ vs_ occur_exactly_in nth_ 1 [c_2 = 0, c + c_2 = 1]" then ()
61 else error "termC.sml subst_atomic_all should be 'false'";
62 ===== inhibit exn ============================================================*)
65 "----------- Pattern.match ------------------------------";
66 "----------- Pattern.match ------------------------------";
67 "----------- Pattern.match ------------------------------";
68 (*===== inhibit exn ============================================================
69 val t = (term_of o the o (parse thy)) "3 * x^^^2 = 1";
70 val pat = (free2var o term_of o the o (parse thy)) "a * b^^^2 = c";
71 (* !^^^^^^^^!... necessary for Pattern.match*)
72 val insts = Pattern.match (Sign.tsig_of (sign_of thy)) (pat, t);
75 [(("c",0),Free ("1","RealDef.real")),(("b",0),Free ("x","RealDef.real")),
76 (("a",0),Free ("3","RealDef.real"))])
77 : (indexname * typ) list * (indexname * term) list*)
79 "----- throws exn MATCH...";
81 (Pattern.match (Sign.tsig_of (sign_of thy)) (pat, t))
82 handle MATCH => ([(* (Term.indexname * Term.typ) *)],
83 [(* (Term.indexname * Term.term) *)]);
86 val thy = @{theory "Complex_Main"};
87 val PARSE = Syntax.read_term_global thy;
88 val (pa, tm) = (PARSE "a + b::real", PARSE "x + 2*z::real");
91 (Vartab.empty : Type.tyenv, Vartab.empty : Envir.tenv);
93 val (tye, tme) = Pattern.match thy (Logic.varify_global pa, tm) (Vartab.empty,
96 val (tyenv, tenv) = Pattern.match thy (Logic.varify_global pa, tm)
97 (Vartab.empty, Vartab.empty);
99 match thy tm (Logic.varify pa);
100 ===== inhibit exn ============================================================*)
102 "----------- fun matches --------------------------------";
103 "----------- fun matches --------------------------------";
104 "----------- fun matches --------------------------------";
105 (*test/../Knowledge/polyeq.sml:
106 Where=[Correct "matches (?a = 0) (-8 - 2 * x + x ^^^ 2 = 0)"*)
107 (*test/../Interpret/ptyps.sml:
108 |\nmatches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"],*)
109 val thy = @{theory "Complex_Main"};
112 val pa = Logic.varify_global @{term "a = (0::real)"}; (*<<<<<<<---------------*)
113 tracing "paIsa=..."; atomty pa; tracing "...=paIsa";
115 *** Const (op =, real => real => bool)
116 *** . Var ((a, 0), real)
117 *** . Const (Groups.zero_class.zero, real)
119 "----- test 1a true";
120 val tm = @{term "-8 - 2 * x + x ^ 2 = (0::real)"}; (*<<<<<<<---------------*)
121 if matches thy tm pa then ()
122 else error "termC.sml diff.behav. in matches true 1";
123 "----- test 1b false";
124 val tm = @{term "-8 - 2 * x + x ^ 2 = (3::real)"}; (*<<<<<<<---------------*)
125 if matches thy tm pa then error "termC.sml diff.behav. in matches false 1"
129 val pa = Logic.varify_global (str2term "a = (0::real)");(*<<<<<<<-------------*)
130 tracing "paLo2=..."; atomty pa; tracing "...=paLo2";
132 *** Const (op =, real => real => bool)
133 *** . Var ((a, 0), real)
134 *** . Var ((0, 0), real)
136 "----- test 2a true";
137 val tm = str2term "-8 - 2 * x + x ^ 2 = (0::real)"; (*<<<<<<<-------------*)
138 if matches thy tm pa then ()
139 else error "termC.sml diff.behav. in matches true 2";
140 "----- test 2b false";
141 val tm = str2term "-8 - 2 * x + x ^ 2 = (3::real)"; (*<<<<<<<-------------*)
142 if matches thy tm pa then ()
143 else error "termC.sml diff.behav. in matches false 2";
144 (* i.e. !!!!!!!!!!!!!!!!! THIS KIND OF PATTERN IS NOT RELIABLE !!!!!!!!!!!!!!!!!
145 if matches thy tm pa then error "termC.sml diff.behav. in matches false 2"
149 val pa = free2var (str2term "a = (0::real)");(*<<<<<<<-------------*)
150 tracing "paF2=..."; atomty pa; tracing "...=paF2";
152 *** Const (op =, real => real => bool)
153 *** . Var ((a, 0), real)
156 "----- test 3a true";
157 val tm = str2term "-8 - 2 * x + x ^ 2 = (0::real)"; (*<<<<<<<-------------*)
158 if matches thy tm pa then ()
159 else error "termC.sml diff.behav. in matches true 3";
160 "----- test 3b false";
161 val tm = str2term "-8 - 2 * x + x ^ 2 = (3::real)"; (*<<<<<<<-------------*)
162 if matches thy tm pa then error "termC.sml diff.behav. in matches false 3"
165 "----- test 4=3 with specific data";
166 val pa = free2var (str2term "M_b 0");
167 "----- test 4a true";
168 val tm = str2term "M_b 0";
169 if matches thy tm pa then ()
170 else error "termC.sml diff.behav. in matches true 4";
171 "----- test 4b false";
172 val tm = str2term "M_b x";
173 if matches thy tm pa then error "termC.sml diff.behav. in matches false 4"
177 "------------parse---------------------------------------";
178 "------------parse---------------------------------------";
179 "------------parse---------------------------------------";
180 Toplevel.debug := true;
182 PolyML.addPrettyPrinter
183 (fn _ => fn _ => ml_pretty o Pretty.to_ML o raw_pp_typ);
185 PolyML.addPrettyPrinter
186 (fn _ => fn _ => ml_pretty o Pretty.to_ML o Proof_Display.pp_typ Pure.thy);
189 val thy = @{theory "Complex_Main"};
194 val t = (Syntax.read_term_global thy str);
195 val t = numbers_to_string (Syntax.read_term_global thy str);
196 val t = (typ_a2real o numbers_to_string) (Syntax.read_term_global thy str);
198 val t = (the (parse thy str)) handle _ => error "termC.sml parsing 'x + 2*z' failed";
201 ML {* @{term "2::int"} *}
203 term "(1.24444) :: real"
205 ML {* numbers_to_string @{term "%x. (-9993::int) + x + 1"} *}
209 "----------- uminus_to_string ---------------------------";
210 "----------- uminus_to_string ---------------------------";
211 "----------- uminus_to_string ---------------------------";
212 val t1 = numbers_to_string @{term "-2::real"};
213 val t2 = numbers_to_string @{term "- 2::real"};
214 if uminus_to_string t2 = t1 then ()
215 else error "termC.sml diff.behav. in uminus_to_string";
218 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.
219 -.-.-.-.-.-.-isolate response.-.-.-.-.-.*)