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