neuper@37906
|
1 |
(* tests on Scripts/term_G.sml
|
neuper@37906
|
2 |
author: Walther Neuper
|
neuper@37906
|
3 |
051006,
|
neuper@37906
|
4 |
(c) due to copyright terms
|
neuper@37906
|
5 |
|
neuper@37906
|
6 |
use"../smltest/Scripts/term_G.sml";
|
neuper@37906
|
7 |
use"term_G.sml";
|
neuper@37906
|
8 |
*)
|
neuper@37906
|
9 |
|
neuper@37906
|
10 |
"-----------------------------------------------------------------";
|
neuper@37906
|
11 |
"table of contents -----------------------------------------------";
|
neuper@37906
|
12 |
"-----------------------------------------------------------------";
|
neuper@37906
|
13 |
"----------- inst_bdv --------------------------------------------";
|
neuper@37906
|
14 |
"----------- subst_atomic_all ------------------------------------";
|
neuper@37906
|
15 |
"----------- Pattern.match ---------------------------------------";
|
neuper@37906
|
16 |
"----------- fun matches -----------------------------------------";
|
neuper@37906
|
17 |
"------------parse------------------------------------------------";
|
neuper@37906
|
18 |
"----------- uminus_to_string ------------------------------------";
|
neuper@37906
|
19 |
"-----------------------------------------------------------------";
|
neuper@37906
|
20 |
"-----------------------------------------------------------------";
|
neuper@37906
|
21 |
|
neuper@37906
|
22 |
|
neuper@37906
|
23 |
"----------- inst_bdv --------------------------------------------";
|
neuper@37906
|
24 |
"----------- inst_bdv --------------------------------------------";
|
neuper@37906
|
25 |
"----------- inst_bdv --------------------------------------------";
|
neuper@37967
|
26 |
if string_of_thm (num_str @{d1_isolate_add2) =
|
neuper@37906
|
27 |
"\"~ ?bdv occurs_in ?a ==> (?a + ?bdv = 0) = (?bdv = -1 * ?a)\"" then ()
|
neuper@37906
|
28 |
else raise error "term_G.sml d1_isolate_add2";
|
neuper@37906
|
29 |
val subst = [(str2term "bdv", str2term "x")];
|
neuper@37967
|
30 |
val t = (norm o #prop o rep_thm) (num_str @{d1_isolate_add2);
|
neuper@37906
|
31 |
val t' = inst_bdv subst t;
|
neuper@37906
|
32 |
if term2str t' = "~ x occurs_in ?a ==> (?a + x = 0) = (x = -1 * ?a)" then ()
|
neuper@37906
|
33 |
else raise error "term_G.sml inst_bdv 1";
|
neuper@37906
|
34 |
|
neuper@37967
|
35 |
if string_of_thm (num_str @{separate_bdvs_add) =
|
neuper@37906
|
36 |
"\"[] from_ [?bdv_1.0, ?bdv_2.0, ?bdv_3.0, ?bdv_4.0] occur_exactly_in ?a\n\
|
neuper@37906
|
37 |
\ ==> (?a + ?b = ?c) = (?b = ?c + -1 * ?a)\"" then ()
|
neuper@37906
|
38 |
else raise error "term_G.sml separate_bdvs_add";
|
neuper@37906
|
39 |
val subst = [(str2term"bdv_1",str2term"c"),
|
neuper@37906
|
40 |
(str2term"bdv_2",str2term"c_2"),
|
neuper@37906
|
41 |
(str2term"bdv_3",str2term"c_3"),
|
neuper@37906
|
42 |
(str2term"bdv_4",str2term"c_4")];
|
neuper@37967
|
43 |
val t = (norm o #prop o rep_thm) (num_str @{separate_bdvs_add);
|
neuper@37906
|
44 |
val t' = inst_bdv subst t;
|
neuper@37906
|
45 |
if term2str t' = "[] from_ [c, c_2, c_3, c_4] occur_exactly_in ?a\n\
|
neuper@37906
|
46 |
\==> (?a + ?b = ?c) = (?b = ?c + -1 * ?a)" then ()
|
neuper@37906
|
47 |
else raise error "term_G.sml inst_bdv 2";
|
neuper@37906
|
48 |
|
neuper@37906
|
49 |
|
neuper@37906
|
50 |
"----------- subst_atomic_all ------------------------------------";
|
neuper@37906
|
51 |
"----------- subst_atomic_all ------------------------------------";
|
neuper@37906
|
52 |
"----------- subst_atomic_all ------------------------------------";
|
neuper@37906
|
53 |
val t = str2term"(tl vs_) from_ vs_ occur_exactly_in (nth_ 1(es_::bool list))";
|
neuper@37906
|
54 |
val env = [(str2term"vs_::real list",str2term"[c, c_2]"),
|
neuper@37906
|
55 |
(str2term"es_::bool list",str2term"[c_2=0, c+c_2=1]")];
|
neuper@37906
|
56 |
val (all_Free_subst, t') = subst_atomic_all env t;
|
neuper@37906
|
57 |
if all_Free_subst andalso
|
neuper@37906
|
58 |
term2str t' = "tl [c, c_2] from_ [c, c_2] occur_exactly_in nth_ 1 [c_2 = 0, c + c_2 = 1]" then ()
|
neuper@37906
|
59 |
else raise error "term_G.sml subst_atomic_all should be 'true'";
|
neuper@37906
|
60 |
|
neuper@37906
|
61 |
|
neuper@37906
|
62 |
val (all_Free_subst, t') = subst_atomic_all (tl env) t;
|
neuper@37906
|
63 |
if not all_Free_subst andalso
|
neuper@37906
|
64 |
term2str t' = "tl vs_ from_ vs_ occur_exactly_in nth_ 1 [c_2 = 0, c + c_2 = 1]" then ()
|
neuper@37906
|
65 |
else raise error "term_G.sml subst_atomic_all should be 'false'";
|
neuper@37906
|
66 |
|
neuper@37906
|
67 |
|
neuper@37906
|
68 |
"----------- Pattern.match ---------------------------------------";
|
neuper@37906
|
69 |
"----------- Pattern.match ---------------------------------------";
|
neuper@37906
|
70 |
"----------- Pattern.match ---------------------------------------";
|
neuper@37906
|
71 |
val t = (term_of o the o (parse thy)) "3 * x^^^2 = 1";
|
neuper@37906
|
72 |
val pat = (free2var o term_of o the o (parse thy)) "a * b^^^2 = c";
|
neuper@37906
|
73 |
(* !^^^^^^^^!... necessary for Pattern.match*)
|
neuper@37906
|
74 |
val insts = Pattern.match (Sign.tsig_of (sign_of thy)) (pat, t);
|
neuper@37906
|
75 |
(*val insts =
|
neuper@37906
|
76 |
([],
|
neuper@37906
|
77 |
[(("c",0),Free ("1","RealDef.real")),(("b",0),Free ("x","RealDef.real")),
|
neuper@37906
|
78 |
(("a",0),Free ("3","RealDef.real"))])
|
neuper@37906
|
79 |
: (indexname * typ) list * (indexname * term) list*)
|
neuper@37906
|
80 |
|
neuper@37906
|
81 |
"----- throws exn MATCH...";
|
neuper@37906
|
82 |
val t = str2term "x";
|
neuper@37906
|
83 |
(Pattern.match (Sign.tsig_of (sign_of thy)) (pat, t))
|
neuper@37906
|
84 |
handle MATCH => ([(* (Term.indexname * Term.typ) *)],
|
neuper@37906
|
85 |
[(* (Term.indexname * Term.term) *)]);
|
neuper@37906
|
86 |
Pattern.MATCH;
|
neuper@37906
|
87 |
|
neuper@37906
|
88 |
(*ML {**)
|
neuper@37906
|
89 |
val thy = @{theory Complex_Main};
|
neuper@37906
|
90 |
val PARSE = Syntax.read_term_global thy;
|
neuper@37906
|
91 |
val (pa, tm) = (PARSE "a + b::real", PARSE "x + 2*z::real");
|
neuper@37906
|
92 |
"-------";
|
neuper@37906
|
93 |
val (tye, tme) =
|
neuper@37906
|
94 |
(Vartab.empty : Type.tyenv, Vartab.empty : Envir.tenv);
|
neuper@37906
|
95 |
"-------";
|
neuper@37906
|
96 |
val (tye, tme) = Pattern.match thy (Logic.varify pa, tm) (Vartab.empty,
|
neuper@37906
|
97 |
Vartab.empty);
|
neuper@37906
|
98 |
"-------";
|
neuper@37906
|
99 |
val (tyenv, tenv) = Pattern.match thy (Logic.varify pa, tm)
|
neuper@37906
|
100 |
(Vartab.empty, Vartab.empty);
|
neuper@37906
|
101 |
Vartab.dest tenv;
|
neuper@37906
|
102 |
match thy tm (Logic.varify pa);
|
neuper@37906
|
103 |
|
neuper@37906
|
104 |
(**}*)
|
neuper@37906
|
105 |
|
neuper@37906
|
106 |
"----------- fun matches -----------------------------------------";
|
neuper@37906
|
107 |
"----------- fun matches -----------------------------------------";
|
neuper@37906
|
108 |
"----------- fun matches -----------------------------------------";
|
neuper@37906
|
109 |
(*smltest/IsacKnowledge/polyeq.sml:
|
neuper@37906
|
110 |
Where=[Correct "matches (?a = 0) (-8 - 2 * x + x ^^^ 2 = 0)"*)
|
neuper@37906
|
111 |
(*smltest/ME/ptyps.sml:
|
neuper@37906
|
112 |
|\nmatches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"],*)
|
neuper@37906
|
113 |
(*ML {**)
|
neuper@37906
|
114 |
val thy = @{theory Complex_Main};
|
neuper@37906
|
115 |
"----- test 1";
|
neuper@37906
|
116 |
val pa = Logic.varify @{term "a = (0::real)"};
|
neuper@37906
|
117 |
"----- test 1 true";
|
neuper@37906
|
118 |
val tm = @{term "-8 - 2 * x + x ^ 2 = (0::real)"};
|
neuper@37906
|
119 |
if matches thy tm pa then ()
|
neuper@37906
|
120 |
else error "term_G.sml diff.behav. in matches true";
|
neuper@37906
|
121 |
"----- test 2 false";
|
neuper@37906
|
122 |
val tm = @{term "-8 - 2 * x + x ^ 2 = (3::real)"};
|
neuper@37906
|
123 |
if matches thy tm pa then error "term_G.sml diff.behav. in matches false"
|
neuper@37906
|
124 |
else ();
|
neuper@37906
|
125 |
(**}*)
|
neuper@37906
|
126 |
|
neuper@37906
|
127 |
"------------parse------------------------------------------------";
|
neuper@37906
|
128 |
"------------parse------------------------------------------------";
|
neuper@37906
|
129 |
"------------parse------------------------------------------------";
|
neuper@37906
|
130 |
(*ML {**)
|
neuper@37906
|
131 |
Toplevel.debug := true;
|
neuper@37906
|
132 |
(* literal types:
|
neuper@37906
|
133 |
PolyML.addPrettyPrinter
|
neuper@37906
|
134 |
(fn _ => fn _ => ml_pretty o Pretty.to_ML o raw_pp_typ);
|
neuper@37906
|
135 |
*)(* pretty types:
|
neuper@37906
|
136 |
PolyML.addPrettyPrinter
|
neuper@37906
|
137 |
(fn _ => fn _ => ml_pretty o Pretty.to_ML o Proof_Display.pp_typ Pure.thy);
|
neuper@37906
|
138 |
print_depth 99;
|
neuper@37906
|
139 |
*)
|
neuper@37906
|
140 |
val thy = @{theory Complex_Main};
|
neuper@37906
|
141 |
val str = "x + z";
|
neuper@37906
|
142 |
parse thy str;
|
neuper@37906
|
143 |
"---------------";
|
neuper@37906
|
144 |
val str = "x + 2*z";
|
neuper@37906
|
145 |
val t = (Syntax.read_term_global thy str);
|
neuper@37906
|
146 |
val t = numbers_to_string (Syntax.read_term_global thy str);
|
neuper@37906
|
147 |
val t = (typ_a2real o numbers_to_string) (Syntax.read_term_global thy str);
|
neuper@37906
|
148 |
cterm_of thy t;
|
neuper@37906
|
149 |
val t = (the (parse thy str)) handle _ => error "term_G.sml parsing 'x + 2*z' failed";
|
neuper@37906
|
150 |
(**}*)
|
neuper@37906
|
151 |
(*Makarius.1003
|
neuper@37906
|
152 |
ML {* @{term "2::int"} *}
|
neuper@37906
|
153 |
|
neuper@37906
|
154 |
term "(1.24444) :: real"
|
neuper@37906
|
155 |
|
neuper@37906
|
156 |
ML {* numbers_to_string @{term "%x. (-9993::int) + x + 1"} *}
|
neuper@37906
|
157 |
*)
|
neuper@37906
|
158 |
|
neuper@37906
|
159 |
|
neuper@37906
|
160 |
"----------- uminus_to_string ------------------------------------";
|
neuper@37906
|
161 |
"----------- uminus_to_string ------------------------------------";
|
neuper@37906
|
162 |
"----------- uminus_to_string ------------------------------------";
|
neuper@37906
|
163 |
(*ML {*)
|
neuper@37906
|
164 |
val t1 = numbers_to_string @{term "-2::real"};
|
neuper@37906
|
165 |
val t2 = numbers_to_string @{term "- 2::real"};
|
neuper@37906
|
166 |
if uminus_to_string t2 = t1 then ()
|
neuper@37906
|
167 |
else error "term_G.sml diff.behav. in uminus_to_string";
|
neuper@37906
|
168 |
(*}*)
|