neuper@37906
|
1 |
(* tests on Atools.thy and Atools.ML
|
neuper@37906
|
2 |
author: Walther Neuper
|
neuper@37906
|
3 |
050814, 08:51
|
neuper@37906
|
4 |
(c) due to copyright terms
|
neuper@37906
|
5 |
|
neuper@37906
|
6 |
use"../smltest/IsacKnowledge/atools.sml";
|
neuper@37906
|
7 |
use"atools.sml";
|
neuper@37906
|
8 |
*)
|
neuper@37906
|
9 |
|
neuper@37906
|
10 |
"-----------------------------------------------------------------";
|
neuper@37906
|
11 |
"table of contents -----------------------------------------------";
|
neuper@37906
|
12 |
"-----------------------------------------------------------------";
|
neuper@37906
|
13 |
"----------- occurs_in -------------------------------------------";
|
neuper@37906
|
14 |
"----------- argument_of -----------------------------------------";
|
neuper@37906
|
15 |
"----------- sameFunId -------------------------------------------";
|
neuper@37906
|
16 |
"----------- filter_sameFunId ------------------------------------";
|
neuper@37906
|
17 |
"----------- boollist2sum ----------------------------------------";
|
neuper@37906
|
18 |
"-----------------------------------------------------------------";
|
neuper@37906
|
19 |
|
neuper@37906
|
20 |
|
neuper@37906
|
21 |
val thy = Atools.thy;
|
neuper@37906
|
22 |
|
neuper@37906
|
23 |
"----------- occurs_in -------------------------------------------";
|
neuper@37906
|
24 |
"----------- occurs_in -------------------------------------------";
|
neuper@37906
|
25 |
"----------- occurs_in -------------------------------------------";
|
neuper@37924
|
26 |
fun str2term str = (term_of o the o (parse thy )) str;
|
neuper@37906
|
27 |
fun term2s t = Sign.string_of_term (sign_of thy) t;
|
neuper@37924
|
28 |
val t = str2term "x";
|
neuper@37906
|
29 |
if occurs_in t t then "OK" else raise error "atools.sml: occurs_in x x -> f";
|
neuper@37906
|
30 |
|
neuper@37906
|
31 |
val t = str2term "x occurs_in x";
|
neuper@37926
|
32 |
val SOME (str, t') = eval_occurs_in 0 "Atools.occurs'_in" t 0;
|
neuper@37906
|
33 |
if (term2s t') = "x occurs_in x = True" then ()
|
neuper@37906
|
34 |
else raise error "atools.sml: x occurs_in x = True ???";
|
neuper@37906
|
35 |
|
neuper@37906
|
36 |
"------- some_occur_in";
|
neuper@37906
|
37 |
some_occur_in [str2term"c",str2term"c_2"] (str2term"a + b + c");
|
neuper@37906
|
38 |
val t = str2term "some_of [c, c_2, c_3, c_4] occur_in \
|
neuper@37906
|
39 |
\-1 * q_0 * L ^^^ 2 / 2 + L * c + c_2";
|
neuper@37926
|
40 |
val SOME (str,t') = eval_some_occur_in 0 "Atools.some'_occur'_in" t 0;
|
neuper@37906
|
41 |
if term2str t' =
|
neuper@37906
|
42 |
"some_of [c, c_2, c_3, c_4] occur_in -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2 =\nTrue" then ()
|
neuper@37906
|
43 |
else raise error "atools.sml: some_occur_in true";
|
neuper@37906
|
44 |
|
neuper@37906
|
45 |
val t = str2term "some_of [c_3, c_4] occur_in \
|
neuper@37906
|
46 |
\-1 * q_0 * L ^^^ 2 / 2 + L * c + c_2";
|
neuper@37926
|
47 |
val SOME (str,t') = eval_some_occur_in 0 "Atools.some'_occur'_in" t 0;
|
neuper@37906
|
48 |
if term2str t' =
|
neuper@37906
|
49 |
"some_of [c_3, c_4] occur_in -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2 = False" then ()
|
neuper@37906
|
50 |
else raise error "atools.sml: some_occur_in false";
|
neuper@37906
|
51 |
|
neuper@37906
|
52 |
|
neuper@37906
|
53 |
"----------- argument_of -----------------------------------------";
|
neuper@37906
|
54 |
"----------- argument_of -----------------------------------------";
|
neuper@37906
|
55 |
"----------- argument_of -----------------------------------------";
|
neuper@37924
|
56 |
val t = str2term "argument_in (M_b x)";
|
neuper@37926
|
57 |
val SOME (str, t') = eval_argument_in 0 "Atools.argument'_in" t 0;
|
neuper@37906
|
58 |
if term2s t' = "(argument_in M_b x) = x" then ()
|
neuper@37906
|
59 |
else raise error "atools.sml:(argument_in M_b x) = x ???";
|
neuper@37906
|
60 |
|
neuper@37906
|
61 |
"----------- sameFunId -------------------------------------------";
|
neuper@37906
|
62 |
"----------- sameFunId -------------------------------------------";
|
neuper@37906
|
63 |
"----------- sameFunId -------------------------------------------";
|
neuper@37906
|
64 |
val t = str2term "M_b L"; atomty t;
|
neuper@37906
|
65 |
val t as f1 $ _ = str2term "M_b L";
|
neuper@37906
|
66 |
val t as Const ("op =", _) $ (f2 $ _) $ _ = str2term "M_b x = c + L*x";
|
neuper@37906
|
67 |
f1 = f2 (*true*);
|
neuper@37906
|
68 |
val (p as Const ("Atools.sameFunId",_) $
|
neuper@37906
|
69 |
(f1 $ _) $
|
neuper@37906
|
70 |
(Const ("op =", _) $ (f2 $ _) $ _)) =
|
neuper@37906
|
71 |
str2term "sameFunId (M_b L) (M_b x = c + L*x)";
|
neuper@37906
|
72 |
f1 = f2 (*true*);
|
neuper@37906
|
73 |
eval_sameFunId "" "Atools.sameFunId"
|
neuper@37906
|
74 |
(str2term "sameFunId (M_b L) (M_b x = c + L*x)")""(*true*);
|
neuper@37906
|
75 |
eval_sameFunId "" "Atools.sameFunId"
|
neuper@37906
|
76 |
(str2term "sameFunId (M_b L) ( y' x = c + L*x)")""(*false*);
|
neuper@37906
|
77 |
eval_sameFunId "" "Atools.sameFunId"
|
neuper@37906
|
78 |
(str2term "sameFunId (M_b L) ( y x = c + L*x)")""(*false*);
|
neuper@37906
|
79 |
eval_sameFunId "" "Atools.sameFunId"
|
neuper@37906
|
80 |
(str2term "sameFunId ( y L) (M_b x = c + L*x)")""(*false*);
|
neuper@37906
|
81 |
eval_sameFunId "" "Atools.sameFunId"
|
neuper@37906
|
82 |
(str2term "sameFunId ( y L) ( y x = c + L*x)")""(*true*);
|
neuper@37906
|
83 |
|
neuper@37906
|
84 |
"----------- filter_sameFunId ------------------------------------";
|
neuper@37906
|
85 |
"----------- filter_sameFunId ------------------------------------";
|
neuper@37906
|
86 |
"----------- filter_sameFunId ------------------------------------";
|
neuper@37906
|
87 |
val flhs as (fid $ _) = str2term "y' L";
|
neuper@37906
|
88 |
val fs = str2term "[M_b x = c + L*x, y' x = c + L*x, y x = c + L*x]";
|
neuper@37906
|
89 |
val (p as Const ("Atools.filter'_sameFunId",_) $ (fid $ _) $ fs) =
|
neuper@37906
|
90 |
str2term "filter_sameFunId (y' L) \
|
neuper@37906
|
91 |
\[M_b x = c + L*x, y' x = c + L*x, y x = c + L*x]";
|
neuper@37926
|
92 |
val SOME (str, es) = eval_filter_sameFunId "" "Atools.filter'_sameFunId" p "";
|
neuper@37906
|
93 |
if term2str es = "(filter_sameFunId y' L [M_b x = c + L * x, y' x = c + L * x,\n y x = c + L * x]) =\n[y' x = c + L * x]" then ()
|
neuper@37906
|
94 |
else raise error "atools.slm diff.behav. in filter_sameFunId";
|
neuper@37906
|
95 |
|
neuper@37906
|
96 |
|
neuper@37906
|
97 |
"----------- boollist2sum ----------------------------------------";
|
neuper@37906
|
98 |
"----------- boollist2sum ----------------------------------------";
|
neuper@37906
|
99 |
"----------- boollist2sum ----------------------------------------";
|
neuper@37906
|
100 |
val u_ = str2term "[]";
|
neuper@37906
|
101 |
val u_ = str2term "[b1 = k - 2*q]";
|
neuper@37906
|
102 |
val u_ = str2term "[b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q]";
|
neuper@37906
|
103 |
val ut_ = isalist2list u_;
|
neuper@37906
|
104 |
val sum_ = map lhs ut_;
|
neuper@37906
|
105 |
val t = list2sum sum_;
|
neuper@37906
|
106 |
term2str t;
|
neuper@37906
|
107 |
|
neuper@37906
|
108 |
val t = str2term
|
neuper@37906
|
109 |
"boollist2sum [b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q]";
|
neuper@37906
|
110 |
|
neuper@37906
|
111 |
val p as Const ("Atools.boollist2sum", _) $ (Const ("List.list.Cons", _) $
|
neuper@37906
|
112 |
_ $ _) = t;
|
neuper@37906
|
113 |
|
neuper@37906
|
114 |
|
neuper@37926
|
115 |
val SOME (str, pred) = eval_boollist2sum "" "Atools.boollist2sum" t "";
|
neuper@37906
|
116 |
if term2str pred = "boollist2sum\n [b1 = k - 2 * q, b2 = k - 2 * q, b3 = k - 2 * q, b4 = k - 2 * q] =\nb1 + b2 + b3 + b4" then ()
|
neuper@37906
|
117 |
else raise error "atools.sml diff.behav. in eval_boollist2sum";
|
neuper@37906
|
118 |
|
neuper@37906
|
119 |
trace_rewrite:=true;
|
neuper@37906
|
120 |
val srls_ = append_rls "srls_..Berechnung-erstSymbolisch" e_rls
|
neuper@37906
|
121 |
[Calc ("Atools.boollist2sum", eval_boollist2sum "")];
|
neuper@37906
|
122 |
val t = str2term
|
neuper@37906
|
123 |
"boollist2sum [b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q]";
|
neuper@37926
|
124 |
case rewrite_set_ thy false srls_ t of SOME _ => ()
|
neuper@37906
|
125 |
| _ => raise error "atools.sml diff.rewrite boollist2sum";
|
neuper@37906
|
126 |
trace_rewrite:=false;
|
neuper@37906
|
127 |
|
neuper@37906
|
128 |
|
neuper@37906
|
129 |
(* use"IsacKnowledge/Atools.ML";
|
neuper@37906
|
130 |
use"../smltest/IsacKnowledge/atools.sml";
|
neuper@37906
|
131 |
*) |