1open HolKernel Parse boolLib bossLib
2open intLib binary_ieeeSyntax binary_ieeeLib machine_ieeeTheory
3open testutils
4
5(*
6fun printn s = print (s ^ "\n")
7fun die s = ( printn s; raise ERR "" "" )
8val die = printn
9*)
10
11val () = show_tags := true
12
13(* ------------------------------------------------------------------------ *)
14
15local
16   val s_t = ``1w:word1``
17   val s_f = ``0w:word1``
18   fun s_tf b = if b then s_t else s_f
19in
20   fun float_constants ty =
21      let
22         val p as (t, w) = dest_float_ty ty
23         val itself = boolSyntax.mk_itself (pairSyntax.mk_prod p)
24         fun mk_lit (s, e, f) =
25            mk_floating_point
26              (s_tf s, wordsSyntax.mk_n2w (numLib.term_of_int e, w),
27               wordsSyntax.mk_n2w (numLib.term_of_int f, t))
28      in
29         mk_float_some_qnan (Term.mk_var ("fp_op", mk_fp_op_ty (t, w))) ::
30         List.map (fn f => f itself)
31            [ mk_float_plus_zero, mk_float_minus_zero,
32             mk_float_plus_min, mk_float_top, mk_float_bottom,
33             mk_float_plus_infinity, mk_float_minus_infinity] @
34         List.map mk_lit
35            [(false, 512, 0),
36             (false, 12, 123456)]
37      end
38end
39
40val round_constants =
41   [roundTiesToEven_tm, roundTowardPositive_tm, roundTowardNegative_tm,
42    roundTowardZero_tm]
43
44val round_constants =
45   [roundTiesToEven_tm, roundTowardZero_tm]
46
47fun has_tags tags thm =
48   case Tag.dest_tag (Thm.tag thm) of
49      (ts, []) => Lib.set_eq ts tags
50    | _ => false
51
52fun pr_term tm =
53   ( print "\n"; Lib.with_flag (show_types, true) print_term tm; print "\n" )
54
55fun ok_result1 tm =
56   tm = boolSyntax.T orelse
57   tm = boolSyntax.F orelse
58   tm = nan_tm orelse
59   tm = infinity_tm orelse
60   (case Lib.total dest_float tm of
61       SOME r => is_ground_real r
62     | NONE => false) orelse
63   is_ground_real tm
64
65fun ok_float tm =
66  is_float_plus_infinity tm orelse
67  is_float_minus_infinity tm orelse
68  is_float_some_qnan tm orelse
69  Lib.can dest_floating_point tm
70
71fun ok_result2 tm =
72   case Lib.total pairSyntax.dest_pair tm of
73      SOME (_, t) => ok_float t
74    | NONE => ok_float tm
75
76fun ok_order_result tm =
77   tm = boolSyntax.T orelse
78   tm = boolSyntax.F orelse
79   tm = EQ_tm orelse
80   tm = GT_tm orelse
81   tm = LT_tm orelse
82   tm = UN_tm
83
84fun test_monops ty =
85   let
86      val cs = float_constants ty
87   in
88      print "\nChecking type: "
89    ; print_type ty
90    ; List.app
91        (fn (name, monop) =>
92         ( print ("\n\nTesting operation: " ^ name ^ "\n")
93         ; List.app
94              (fn a =>
95                 let
96                    val tm =
97                       monop a handle e as HOL_ERR _ => (pr_term a; raise e)
98                    val e1 = EVAL tm
99                    val r = rhs (concl e1)
100                 in
101                    if ok_result1 r orelse ok_result2 r orelse
102                       Lib.mem name ["float_negate", "float_abs"] andalso
103                       is_float_some_qnan a
104                       then print "."
105                    else ( print "\n"
106                         ; print_thm e1
107                         ; print "\n"
108                         ; die "test_monops failed"
109                         )
110                 end) cs))
111        [("float_negate", mk_float_negate),
112         ("float_abs", mk_float_abs),
113         ("float_value", mk_float_value),
114         ("float_is_nan", mk_float_is_nan),
115         ("float_is_signalling", mk_float_is_signalling),
116         ("float_is_infinite", mk_float_is_infinite),
117         ("float_is_finite", mk_float_is_finite),
118         ("float_is_normal", mk_float_is_normal),
119         ("float_is_subnormal", mk_float_is_subnormal),
120         ("float_is_zero", mk_float_is_zero)
121        ]
122    ; print "\nDone.\n"
123   end
124
125fun test_binops ty =
126   let
127      val cs = float_constants ty
128   in
129      print "\nChecking type: "
130    ; print_type ty
131    ; List.app
132        (fn (name, binop) =>
133         ( print ("\n\nTesting operation: " ^ name ^ "\n")
134         ; List.app
135              (fn mode =>
136               ( print "\nMode: "; print_term mode; print "\n"
137               ; List.app
138                    (fn a =>
139                       List.app
140                          (fn b =>
141                             let
142                                val tm = binop (mode, a, b)
143                                         handle e as HOL_ERR _ =>
144                                           ( pr_term mode
145                                           ; pr_term a
146                                           ; pr_term b
147                                           ; raise e
148                                           )
149                                val e1 = EVAL tm
150                                val r = rhs (concl e1)
151                             in
152                                if ok_result2 r
153                                   then print "."
154                                else ( print "\n"
155                                     ; print_thm e1
156                                     ; print "\n"
157                                     ; die "test_binops failed"
158                                     )
159                             end) cs) cs)) round_constants))
160        [("float_add", mk_float_add), ("float_sub", mk_float_sub),
161         ("float_mul", mk_float_mul), ("float_div", mk_float_div)
162        ]
163    ; print "\nDone.\n"
164   end
165
166fun test_orderings ty =
167   let
168      val cs = float_constants ty
169   in
170      print "\nChecking type: "
171    ; print_type ty
172    ; List.app
173        (fn (name, binop) =>
174         ( print ("\n\nTesting operation: " ^ name ^ "\n")
175         ; List.app
176              (fn a =>
177                 List.app
178                    (fn b =>
179                       let
180                          val tm = binop (a, b)
181                                   handle e as HOL_ERR _ =>
182                                     ( pr_term a
183                                     ; pr_term b
184                                     ; raise e
185                                     )
186                          val e1 = EVAL tm
187                          val r = rhs (concl e1)
188                       in
189                          if ok_order_result r
190                             then print "."
191                          else ( print "\n"
192                               ; print_thm e1
193                               ; print "\n"
194                               ; die "test_orderings failed"
195                               )
196                       end) cs) cs))
197        [("float_less_than", mk_float_less_than),
198         ("float_less_equal", mk_float_less_equal),
199         ("float_greater_than", mk_float_greater_than),
200         ("float_greater_equal", mk_float_greater_equal),
201         ("float_equal", mk_float_equal),
202         ("float_compare", mk_float_compare)]
203    ; print "\nDone.\n"
204   end
205
206(* ------------------------------------------------------------------------ *)
207
208(* start tests *)
209val tt = Timer.startRealTimer ()
210
211val () = test_monops ``:half``
212val () = test_binops ``:half``
213val () = test_orderings ``:half``
214
215val () = test_monops ``:single``
216val () = test_binops ``:single``
217val () = test_orderings ``:single``
218
219val elapsed = Timer.checkRealTimer tt;
220
221val _ = print ("\nTotal time: " ^ Lib.time_to_string elapsed ^ "\n")
222
223(* ------------------------------------------------------------------------ *)
224
225val _ = OS.Process.exit OS.Process.success
226