|
1 (* Title: tests on ProgLang/termC.sml |
|
2 Author: Walther Neuper 051006, |
|
3 (c) due to copyright terms |
|
4 *) |
|
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 "--------------------------------------------------------"; |
|
16 |
|
17 |
|
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 raise 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 raise error "termC.sml inst_bdv 1"; |
|
30 |
|
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 raise 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 raise error "termC.sml inst_bdv 2"; |
|
44 |
|
45 |
|
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 raise error "termC.sml subst_atomic_all should be 'true'"; |
|
56 |
|
57 |
|
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 raise error "termC.sml subst_atomic_all should be 'false'"; |
|
62 ===== inhibit exn ============================================================*) |
|
63 |
|
64 |
|
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); |
|
73 (*val insts = |
|
74 ([], |
|
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*) |
|
78 |
|
79 "----- throws exn MATCH..."; |
|
80 val t = str2term "x"; |
|
81 (Pattern.match (Sign.tsig_of (sign_of thy)) (pat, t)) |
|
82 handle MATCH => ([(* (Term.indexname * Term.typ) *)], |
|
83 [(* (Term.indexname * Term.term) *)]); |
|
84 Pattern.MATCH; |
|
85 |
|
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"); |
|
89 "-------"; |
|
90 val (tye, tme) = |
|
91 (Vartab.empty : Type.tyenv, Vartab.empty : Envir.tenv); |
|
92 "-------"; |
|
93 val (tye, tme) = Pattern.match thy (Logic.varify_global pa, tm) (Vartab.empty, |
|
94 Vartab.empty); |
|
95 "-------"; |
|
96 val (tyenv, tenv) = Pattern.match thy (Logic.varify_global pa, tm) |
|
97 (Vartab.empty, Vartab.empty); |
|
98 Vartab.dest tenv; |
|
99 match thy tm (Logic.varify pa); |
|
100 ===== inhibit exn ============================================================*) |
|
101 |
|
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"}; |
|
110 |
|
111 "----- test 1: OK"; |
|
112 val pa = Logic.varify_global @{term "a = (0::real)"}; (*<<<<<<<---------------*) |
|
113 tracing "paIsa=..."; atomty pa; tracing "...=paIsa"; |
|
114 (*** |
|
115 *** Const (op =, real => real => bool) |
|
116 *** . Var ((a, 0), real) |
|
117 *** . Const (Groups.zero_class.zero, real) |
|
118 ***) |
|
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" |
|
126 else (); |
|
127 |
|
128 "----- test 2: Nok"; |
|
129 val pa = Logic.varify_global (str2term "a = (0::real)");(*<<<<<<<-------------*) |
|
130 tracing "paLo2=..."; atomty pa; tracing "...=paLo2"; |
|
131 (*** |
|
132 *** Const (op =, real => real => bool) |
|
133 *** . Var ((a, 0), real) |
|
134 *** . Var ((0, 0), real) |
|
135 ***) |
|
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" |
|
146 else ();*) |
|
147 |
|
148 "----- test 3: OK"; |
|
149 val pa = free2var (str2term "a = (0::real)");(*<<<<<<<-------------*) |
|
150 tracing "paF2=..."; atomty pa; tracing "...=paF2"; |
|
151 (*** |
|
152 *** Const (op =, real => real => bool) |
|
153 *** . Var ((a, 0), real) |
|
154 *** . Free (0, real) |
|
155 ***) |
|
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" |
|
163 else (); |
|
164 |
|
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" |
|
174 else (); |
|
175 |
|
176 |
|
177 "------------parse---------------------------------------"; |
|
178 "------------parse---------------------------------------"; |
|
179 "------------parse---------------------------------------"; |
|
180 Toplevel.debug := true; |
|
181 (* literal types: |
|
182 PolyML.addPrettyPrinter |
|
183 (fn _ => fn _ => ml_pretty o Pretty.to_ML o raw_pp_typ); |
|
184 *)(* pretty types: |
|
185 PolyML.addPrettyPrinter |
|
186 (fn _ => fn _ => ml_pretty o Pretty.to_ML o Proof_Display.pp_typ Pure.thy); |
|
187 print_depth 99; |
|
188 *) |
|
189 val thy = @{theory "Complex_Main"}; |
|
190 val str = "x + z"; |
|
191 parse thy str; |
|
192 "---------------"; |
|
193 val str = "x + 2*z"; |
|
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); |
|
197 cterm_of thy t; |
|
198 val t = (the (parse thy str)) handle _ => error "termC.sml parsing 'x + 2*z' failed"; |
|
199 |
|
200 (*Makarius.1003 |
|
201 ML {* @{term "2::int"} *} |
|
202 |
|
203 term "(1.24444) :: real" |
|
204 |
|
205 ML {* numbers_to_string @{term "%x. (-9993::int) + x + 1"} *} |
|
206 *) |
|
207 |
|
208 |
|
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"; |
|
216 |
|
217 |
|
218 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-. |
|
219 -.-.-.-.-.-.-isolate response.-.-.-.-.-.*) |