1 (* tests on Atools.thy and Atools.ML
4 (c) due to copyright terms
6 use"../smltest/IsacKnowledge/atools.sml";
10 "-----------------------------------------------------------------";
11 "table of contents -----------------------------------------------";
12 "-----------------------------------------------------------------";
13 "----------- occurs_in -------------------------------------------";
14 "----------- argument_of -----------------------------------------";
15 "----------- sameFunId -------------------------------------------";
16 "----------- filter_sameFunId ------------------------------------";
17 "----------- boollist2sum ----------------------------------------";
18 "-----------------------------------------------------------------";
23 "----------- occurs_in -------------------------------------------";
24 "----------- occurs_in -------------------------------------------";
25 "----------- occurs_in -------------------------------------------";
26 fun str2term str = (term_of o the o (parse thy )) str;
27 fun term2s t = Syntax.string_of_term (thy2ctxt thy) t;
29 if occurs_in t t then "OK" else raise error "atools.sml: occurs_in x x -> f";
31 val t = str2term "x occurs_in x";
32 val SOME (str, t') = eval_occurs_in 0 "Atools.occurs'_in" t 0;
33 if (term2s t') = "x occurs_in x = True" then ()
34 else raise error "atools.sml: x occurs_in x = True ???";
36 "------- some_occur_in";
37 some_occur_in [str2term"c",str2term"c_2"] (str2term"a + b + c");
38 val t = str2term "some_of [c, c_2, c_3, c_4] occur_in \
39 \-1 * q_0 * L ^^^ 2 / 2 + L * c + c_2";
40 val SOME (str,t') = eval_some_occur_in 0 "Atools.some'_occur'_in" t 0;
42 "some_of [c, c_2, c_3, c_4] occur_in -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2 =\nTrue" then ()
43 else raise error "atools.sml: some_occur_in true";
45 val t = str2term "some_of [c_3, c_4] occur_in \
46 \-1 * q_0 * L ^^^ 2 / 2 + L * c + c_2";
47 val SOME (str,t') = eval_some_occur_in 0 "Atools.some'_occur'_in" t 0;
49 "some_of [c_3, c_4] occur_in -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2 = False" then ()
50 else raise error "atools.sml: some_occur_in false";
53 "----------- argument_of -----------------------------------------";
54 "----------- argument_of -----------------------------------------";
55 "----------- argument_of -----------------------------------------";
56 val t = str2term "argument_in (M_b x)";
57 val SOME (str, t') = eval_argument_in 0 "Atools.argument'_in" t 0;
58 if term2s t' = "(argument_in M_b x) = x" then ()
59 else raise error "atools.sml:(argument_in M_b x) = x ???";
61 "----------- sameFunId -------------------------------------------";
62 "----------- sameFunId -------------------------------------------";
63 "----------- sameFunId -------------------------------------------";
64 val t = str2term "M_b L"; atomty t;
65 val t as f1 $ _ = str2term "M_b L";
66 val t as Const ("op =", _) $ (f2 $ _) $ _ = str2term "M_b x = c + L*x";
68 val (p as Const ("Atools.sameFunId",_) $
70 (Const ("op =", _) $ (f2 $ _) $ _)) =
71 str2term "sameFunId (M_b L) (M_b x = c + L*x)";
73 eval_sameFunId "" "Atools.sameFunId"
74 (str2term "sameFunId (M_b L) (M_b x = c + L*x)")""(*true*);
75 eval_sameFunId "" "Atools.sameFunId"
76 (str2term "sameFunId (M_b L) ( y' x = c + L*x)")""(*false*);
77 eval_sameFunId "" "Atools.sameFunId"
78 (str2term "sameFunId (M_b L) ( y x = c + L*x)")""(*false*);
79 eval_sameFunId "" "Atools.sameFunId"
80 (str2term "sameFunId ( y L) (M_b x = c + L*x)")""(*false*);
81 eval_sameFunId "" "Atools.sameFunId"
82 (str2term "sameFunId ( y L) ( y x = c + L*x)")""(*true*);
84 "----------- filter_sameFunId ------------------------------------";
85 "----------- filter_sameFunId ------------------------------------";
86 "----------- filter_sameFunId ------------------------------------";
87 val flhs as (fid $ _) = str2term "y' L";
88 val fs = str2term "[M_b x = c + L*x, y' x = c + L*x, y x = c + L*x]";
89 val (p as Const ("Atools.filter'_sameFunId",_) $ (fid $ _) $ fs) =
90 str2term "filter_sameFunId (y' L) \
91 \[M_b x = c + L*x, y' x = c + L*x, y x = c + L*x]";
92 val SOME (str, es) = eval_filter_sameFunId "" "Atools.filter'_sameFunId" p "";
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 ()
94 else raise error "atools.slm diff.behav. in filter_sameFunId";
97 "----------- boollist2sum ----------------------------------------";
98 "----------- boollist2sum ----------------------------------------";
99 "----------- boollist2sum ----------------------------------------";
100 val u_ = str2term "[]";
101 val u_ = str2term "[b1 = k - 2*q]";
102 val u_ = str2term "[b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q]";
103 val ut_ = isalist2list u_;
104 val sum_ = map lhs ut_;
105 val t = list2sum sum_;
109 "boollist2sum [b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q]";
111 val p as Const ("Atools.boollist2sum", _) $ (Const ("List.list.Cons", _) $
115 val SOME (str, pred) = eval_boollist2sum "" "Atools.boollist2sum" t "";
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 ()
117 else raise error "atools.sml diff.behav. in eval_boollist2sum";
120 val srls_ = append_rls "srls_..Berechnung-erstSymbolisch" e_rls
121 [Calc ("Atools.boollist2sum", eval_boollist2sum "")];
123 "boollist2sum [b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q]";
124 case rewrite_set_ thy false srls_ t of SOME _ => ()
125 | _ => raise error "atools.sml diff.rewrite boollist2sum";
126 trace_rewrite:=false;
129 (* use"IsacKnowledge/Atools.ML";
130 use"../smltest/IsacKnowledge/atools.sml";