1open HolKernel Parse boolLib bossLib 2open machine_ieeeLib; 3 4val () = new_theory "machine_ieee"; 5 6(* ------------------------------------------------------------------------ 7 Bit-vector Encodings 8 ------------------------------------------------------------------------ *) 9 10(* 16-bit, 32-bit and 64-bit encodings *) 11 12val thms = (List.concat o List.map machine_ieeeLib.mk_fp_encoding) 13 [("fp16", 10, 5, SOME "half"), 14 ("fp32", 23, 8, SOME "single"), 15 ("fp64", 52, 11, SOME "double")]; 16 17(* ------------------------------------------------------------------------ 18 Encoding conversions 19 ------------------------------------------------------------------------ *) 20 21val convert_def = Define` 22 convert (to_float: 'a word -> ('b, 'c) float) 23 (from_float: ('d, 'e) float -> 'f word) from_real_with_flags 24 (m: rounding) w = 25 let f = to_float w in 26 case float_value f of 27 Float r => from_real_with_flags m r 28 | NaN => (check_for_signalling [f], from_float (@fp. float_is_nan fp)) 29 | Infinity => 30 (clear_flags, 31 from_float (if f.Sign = 0w then 32 float_plus_infinity (:'d # 'e) 33 else 34 float_minus_infinity (:'d # 'e)))` 35 36(* These can only set InvalidOp *) 37 38val fp16_to_fp32_with_flags_def = Define` 39 fp16_to_fp32_with_flags = 40 convert fp16_to_float float_to_fp32 real_to_fp32_with_flags roundTiesToEven` 41 42val fp16_to_fp64_with_flags_def = Define` 43 fp16_to_fp64_with_flags = 44 convert fp16_to_float float_to_fp64 real_to_fp64_with_flags roundTiesToEven` 45 46val fp32_to_fp64_with_flags_def = Define` 47 fp32_to_fp64_with_flags = 48 convert fp32_to_float float_to_fp64 real_to_fp64_with_flags roundTiesToEven` 49 50(* These can set InvalidOp, Overflow, Precision and Underflow_* *) 51 52val fp64_to_fp32_with_flags_def = Define` 53 fp64_to_fp32_with_flags = 54 convert fp64_to_float float_to_fp32 real_to_fp32_with_flags` 55 56val fp64_to_fp16_with_flags_def = Define` 57 fp64_to_fp16_with_flags = 58 convert fp64_to_float float_to_fp16 real_to_fp16_with_flags` 59 60val fp32_to_fp16_with_flags_def = Define` 61 fp32_to_fp16_with_flags = 62 convert fp32_to_float float_to_fp16 real_to_fp16_with_flags` 63 64(* Versions without flags *) 65 66val fp16_to_fp32_def = Define `fp16_to_fp32 = SND o fp16_to_fp32_with_flags` 67val fp16_to_fp64_def = Define `fp16_to_fp64 = SND o fp16_to_fp64_with_flags` 68val fp32_to_fp64_def = Define `fp32_to_fp64 = SND o fp32_to_fp64_with_flags` 69 70val fp64_to_fp32_def = Define `fp64_to_fp32 m = SND o fp64_to_fp32_with_flags m` 71val fp64_to_fp16_def = Define `fp64_to_fp16 m = SND o fp64_to_fp16_with_flags m` 72val fp32_to_fp16_def = Define `fp32_to_fp16 m = SND o fp32_to_fp16_with_flags m` 73 74(* ------------------------------------------------------------------------ 75 Support 64-bit native evaluation 76 (Controlled by the trace "native IEEE". Off by default.) 77 ------------------------------------------------------------------------ *) 78 79val () = Theory.quote_adjoin_to_theory 80`val sqrt_CONV: Conv.conv ref 81val add_CONV: Conv.conv ref 82val sub_CONV: Conv.conv ref 83val mul_CONV: Conv.conv ref 84val div_CONV: Conv.conv ref 85val compare_CONV: Conv.conv ref 86val eq_CONV: Conv.conv ref 87val lt_CONV: Conv.conv ref 88val le_CONV: Conv.conv ref 89val gt_CONV: Conv.conv ref 90val ge_CONV: Conv.conv ref` 91`val native_eval = ref false(* off by default *) 92val () = Feedback.register_btrace ("native IEEE", native_eval) 93val sqrt_CONV = ref Conv.NO_CONV 94val add_CONV = ref Conv.NO_CONV 95val sub_CONV = ref Conv.NO_CONV 96val mul_CONV = ref Conv.NO_CONV 97val div_CONV = ref Conv.NO_CONV 98val compare_CONV = ref Conv.NO_CONV 99val eq_CONV = ref Conv.NO_CONV 100val lt_CONV = ref Conv.NO_CONV 101val le_CONV = ref Conv.NO_CONV 102val gt_CONV = ref Conv.NO_CONV 103val ge_CONV = ref Conv.NO_CONV 104fun native cnv1 s = 105 let 106 val cnv2 = 107 Conv.QCHANGED_CONV 108 (Rewrite.PURE_REWRITE_CONV [DB.fetch "machine_ieee" ("fp64_" ^ s)]) 109 in 110 fn tm => (if !native_eval then !cnv1 else cnv2) tm 111 end 112fun mk s = Term.prim_mk_const {Name = "fp64_" ^ s, Thy = "machine_ieee"} 113val () = computeLib.add_convs 114 [(mk "sqrt", 2, native sqrt_CONV "sqrt"), 115 (mk "add", 3, native add_CONV "add"), 116 (mk "sub", 3, native sub_CONV "sub"), 117 (mk "mul", 3, native mul_CONV "mul"), 118 (mk "div", 3, native div_CONV "div"), 119 (mk "compare", 2, native compare_CONV "compare"), 120 (mk "equal", 2, native eq_CONV "equal"), 121 (mk "lessThan", 2, native lt_CONV "lessThan"), 122 (mk "lessEqual", 2, native le_CONV "lessEqual"), 123 (mk "greaterThan", 2, native gt_CONV "greaterThan"), 124 (mk "greaterEqual", 2, native ge_CONV "greaterEqual") 125 ]` 126 127val () = export_theory () 128