|
1 (* (c) Stefan Rath 2005 |
|
2 tests for sml/Scripts/calculate.sml |
|
3 |
|
4 use"~/proto2/isac/src/smltest/Scripts/calculate-float.sml"; |
|
5 use"calculate-float.sml"; |
|
6 *) |
|
7 |
|
8 |
|
9 (*WN.28.3.03 fuer Matthias*) |
|
10 (*Floatingpointnumbers, direkte Darstellung der abstrakten Syntax:*) |
|
11 val thy = Float.thy; |
|
12 val t = str2term "Float ((1,2),(0,0))"; |
|
13 atomt t; |
|
14 val t = (term_of o the o (parse thy)) |
|
15 "Float ((1,2),(0,0)) + Float ((3,4),(0,0)) * \ |
|
16 \Float ((5,6),(0,0)) / Float ((7,8),(0,0))"; |
|
17 atomt t; |
|
18 (*die konkrete Syntax wird noch verschoenert*) |
|
19 |
|
20 val thy = "Test.thy"; |
|
21 val op_ = "divide_"; |
|
22 val ct = "-6 / 3"; |
|
23 val Some (ct,_) = calculate thy (the (assoc (calclist, op_))) ct; |
|
24 |
|
25 (*-----WN050315------------------------------------------------------*) |
|
26 (*..*) |
|
27 val t = str2term "Float ((1,2),(0,0))"; |
|
28 atomty t; |
|
29 val Const ("Float.Float",_) $ |
|
30 (Const ("Pair",_) $ |
|
31 (Const ("Pair",_) $ Free (i1,_) $ Free (i2,_)) $ _) = t; |
|
32 |
|
33 val t = str2term "Float ((1,2),(0,0)) + Float ((3,4),(0,0))"; |
|
34 atomty t; |
|
35 (*-----WN050315------------------------------------------------------*) |
|
36 |
|
37 |
|
38 val thy = Float.thy; |
|
39 |
|
40 (*.calculate the value of a pair of floats.*) |
|
41 val ((a,b),(c,d)) = calc "op +" ((~1,0),(0,0)) ((2,0),(0,0)); |
|
42 |
|
43 |
|
44 (*.build the term.*) |
|
45 term_of_float HOLogic.realT ((~1,0),(0,0)); |
|
46 term_of_float HOLogic.realT ((~1,11),(0,0)); |
|
47 |
|
48 (*--18.3.05-------------------------*) |
|
49 val t = Free ("sdfsdfsdf", HOLogic.realT); |
|
50 val t = Free ("-123,456", HOLogic.realT); |
|
51 val t = Free ("0,123456", HOLogic.realT); |
|
52 term2str t; |
|
53 (*----(1)------------------------------*) |
|
54 val t = str2term "IFloat (1, 2, 3)"; |
|
55 val t = str2term "CFloat (1, 2)"; |
|
56 atomt t; |
|
57 atomty t; |
|
58 val Some ct = parse Float.thy "IFloat (1, 2, 3)"; |
|
59 val Some ct = parse Float.thy "CFloat (1, 2)"; |
|
60 atomt (term_of ct); |
|
61 atomty (term_of ct); |
|
62 (*----(2)------------------------------*) |
|
63 val Some ct = parse Float.thy "IFloat (-1, 2, 3)"; |
|
64 val t = (term_of ct); |
|
65 atomty t; |
|
66 (*#######################################################################3 |
|
67 val Const |
|
68 ("Float.IFloat", _) $ |
|
69 (Const |
|
70 ("Pair", _) $ |
|
71 Free (no, _) $ |
|
72 (Const |
|
73 ("Pair", _) $ |
|
74 Free (commas, _) $ Free (exp, _))) = t; |
|
75 |
|
76 fun IFloat2CFloat |
|
77 (Const |
|
78 ("Float.IFloat", _) $ |
|
79 (Const |
|
80 ("Pair", _) $ |
|
81 Free (no, _) $ |
|
82 (Const |
|
83 ("Pair", _) $ |
|
84 Free (commas, _) $ Free (exp, _)))) = |
|
85 Const ("Float.CFloat", HOLogic.realT(*wrong type*)) $ |
|
86 (Const |
|
87 ("Pair", HOLogic.realT(*wrong type*)) $ |
|
88 Free (no^"."^commas, HOLogic.realT) |
|
89 $ Free ("accuracy", HOLogic.realT)) |
|
90 |
|
91 | IFloat2CFloat t = |
|
92 raise error ("IFloat2CFloat: invalid argument "^term2str t); |
|
93 |
|
94 val cf = IFloat2CFloat t; |
|
95 term2str cf; |
|
96 |
|
97 (*in IsacKnowledge/Float.ML: fun pairt -> Pair-term*) |
|
98 |
|
99 fun CFloat2Free (Const ("Float.CFloat", _) $ |
|
100 (Const ("Pair", _) $ Free (no_commas, _) $ _)) = |
|
101 Free (no_commas, HOLogic.realT); |
|
102 |
|
103 val t' = CFloat2Free cf; |
|
104 term2str t'; |
|
105 |
|
106 fun CFloat2sml (Const ("Float.CFloat", _) $ |
|
107 (Const ("Pair", _) $ Free (float, _) $ _(**))) = |
|
108 float; |
|
109 CFloat2sml cf; |
|
110 |
|
111 (*--18.3.05-------------------------*) |
|
112 |
|
113 |
|
114 (*.the function evaluating a binary operator.*) |
|
115 val t = str2term "Float ((1,2),(0,0)) + Float ((3,4),(0,0))"; |
|
116 val Some (thmid, t) = eval_binop "#add_" "op +" t thy; |
|
117 term2str t; |
|
118 |
|
119 |
|
120 (*.scan a term for a pair of floats.*) |
|
121 val Some (thmid,t') = get_pair thy op_ eval_fn t; |
|
122 |
|
123 |
|
124 (*.use 'calculate' explicitly.*) |
|
125 val thy = Test.thy; |
|
126 val op_ = "divide_"; |
|
127 val t = str2term "sqrt (x ^^^ 2 + -3 * x) =\ |
|
128 \Float ((5,6),(0,0)) / Float ((7,8),(0,0))"; |
|
129 val Some (t',_) = calculate_ thy (the (assoc (calclist, op_))) t; |
|
130 term2str t'; |
|
131 |
|
132 |
|
133 (*.rewrite with ruleset TEST...simplify (calling calculate internally.*) |
|
134 val t = str2term "a + Float ((1,2),(0,0)) + a + Float ((3,4),(0,0)) * \ |
|
135 \Float ((5,6),(0,0)) / Float ((7,8),(0,0))"; |
|
136 val Some (t',_) = rewrite_set_ thy false norm_Rational(*///*) t; term2str t'; |
|
137 (*Float ((...,...) + 2*a*) |
|
138 |
|
139 |
|
140 (*. parse a float as seen by the user .*) |
|
141 val Some t = parse Float.thy "123.456"; |
|
142 val Some t = parse Float.thy "-123.456"; |
|
143 val Some t = parse Float.thy "123.456 E6789"; |
|
144 val Some t = parse Float.thy "123.456 E-6789"; |
|
145 val Some t = parse Float.thy "-123.456 E-6789"; |
|
146 |
|
147 ################################################################*) |