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