-
Notifications
You must be signed in to change notification settings - Fork 85
/
Copy pathfpSem.lem
134 lines (116 loc) · 5.13 KB
/
fpSem.lem
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
(*
Definitions of the floating point operations used in CakeML.
*)
open import Pervasives
open import Lib
open import FpOpt
open import FpValTree
open import {hol} `machine_ieeeTheory`
open import {isabelle} `IEEE_Floating_Point.FP64`
type rounding
declare hol target_rep type rounding = `rounding`
declare isabelle target_rep type rounding = `roundmode`
declare {isabelle} rename type fp_cmp = fp_cmp_op
declare {isabelle} rename type fp_uop = fp_uop_op
declare {isabelle} rename type fp_bop = fp_bop_op
declare {isabelle} rename type fp_top = fp_top_op
(**
This defines the floating-point semantics operating on 64-bit words
**)
val fp64_lessThan : word64 -> word64 -> bool
val fp64_lessEqual : word64 -> word64 -> bool
val fp64_greaterThan : word64 -> word64 -> bool
val fp64_greaterEqual : word64 -> word64 -> bool
val fp64_equal : word64 -> word64 -> bool
declare hol target_rep function fp64_lessThan = `fp64_lessThan`
declare hol target_rep function fp64_lessEqual = `fp64_lessEqual`
declare hol target_rep function fp64_greaterThan = `fp64_greaterThan`
declare hol target_rep function fp64_greaterEqual = `fp64_greaterEqual`
declare hol target_rep function fp64_equal = `fp64_equal`
declare isabelle target_rep function fp64_lessThan = `fp64_lessThan`
declare isabelle target_rep function fp64_lessEqual = `fp64_lessEqual`
declare isabelle target_rep function fp64_greaterThan = `fp64_greaterThan`
declare isabelle target_rep function fp64_greaterEqual = `fp64_greaterEqual`
declare isabelle target_rep function fp64_equal = `fp64_equal`
val fp64_isNan :word64 -> bool
declare hol target_rep function fp64_isNan = `fp64_isNan`
declare isabelle target_rep function fp64_isNan = `fp64_isNan`
val fp64_abs : word64 -> word64
val fp64_negate : word64 -> word64
val fp64_sqrt : rounding -> word64 -> word64
declare hol target_rep function fp64_abs = `fp64_abs`
declare hol target_rep function fp64_negate = `fp64_negate`
declare hol target_rep function fp64_sqrt = `fp64_sqrt`
declare isabelle target_rep function fp64_abs = `fp64_abs`
declare isabelle target_rep function fp64_negate = `fp64_negate`
declare isabelle target_rep function fp64_sqrt = `fp64_sqrt`
val fp64_add : rounding -> word64 -> word64 -> word64
val fp64_sub : rounding -> word64 -> word64 -> word64
val fp64_mul : rounding -> word64 -> word64 -> word64
val fp64_div : rounding -> word64 -> word64 -> word64
declare hol target_rep function fp64_add = `fp64_add`
declare hol target_rep function fp64_sub = `fp64_sub`
declare hol target_rep function fp64_mul = `fp64_mul`
declare hol target_rep function fp64_div = `fp64_div`
declare isabelle target_rep function fp64_add = `fp64_add`
declare isabelle target_rep function fp64_sub = `fp64_sub`
declare isabelle target_rep function fp64_mul = `fp64_mul`
declare isabelle target_rep function fp64_div = `fp64_div`
val fp64_mul_add : rounding -> word64 -> word64 -> word64 -> word64
declare hol target_rep function fp64_mul_add = `fp64_mul_add`
declare isabelle target_rep function fp64_mul_add = `fp64_mul_add`
val roundTiesToEven : rounding
declare hol target_rep function roundTiesToEven = `roundTiesToEven`
declare isabelle target_rep function roundTiesToEven = `To_nearest`
val fp_cmp_comp : fp_cmp -> word64 -> word64 -> bool
let fp_cmp_comp fop = match fop with
| FP_Less -> fp64_lessThan
| FP_LessEqual -> fp64_lessEqual
| FP_Greater -> fp64_greaterThan
| FP_GreaterEqual -> fp64_greaterEqual
| FP_Equal -> fp64_equal
end
(*
val fp_pred_comp : fp_pred -> word64 -> bool
let fp_pred_comp fp = match fp with
| FP_NaN -> fp64_isNan
end
*)
val fp_uop_comp : fp_uop -> word64 -> word64
let fp_uop_comp fop w = match fop with
| FP_Abs -> fp64_abs w
| FP_Neg -> fp64_negate w
| FP_Sqrt -> fp64_sqrt roundTiesToEven w
end
val fp_bop_comp : fp_bop -> word64 -> word64 -> word64
let fp_bop_comp fop = match fop with
| FP_Add -> fp64_add roundTiesToEven
| FP_Sub -> fp64_sub roundTiesToEven
| FP_Mul -> fp64_mul roundTiesToEven
| FP_Div -> fp64_div roundTiesToEven
end
let fpfma v1 v2 v3 = fp64_mul_add roundTiesToEven v2 v3 v1
val fp_top_comp : fp_top -> word64 -> word64 -> word64 -> word64
let fp_top_comp fop = match fop with
| FP_Fma -> fpfma
end
val fp_opt_comp: forall 'v. fp_opt -> 'v -> 'v
let fp_opt_comp sc v = match sc with
| Opt -> v
| NoOpt -> v
end
(* Compression function for value trees,
evaluating lazy trees into word64 or bool *)
val compress_word: fp_word_val -> word64
let rec compress_word (Fp_const w1) = w1
and compress_word (Fp_uop u1 v1) = fp_uop_comp u1 (compress_word v1)
and compress_word (Fp_bop b v1 v2) =
fp_bop_comp b (compress_word v1) (compress_word v2)
and compress_word (Fp_top t v1 v2 v3) =
(fp_top_comp t (compress_word v1) (compress_word v2) (compress_word v3))
and compress_word (Fp_wopt sc v) = compress_word v
val compress_bool : fp_bool_val -> bool
let rec (* compress_bool (Fp_pred p v1) = fp_pred_comp p (compress_word v1)
and *) compress_bool (Fp_cmp cmp v1 v2) =
fp_cmp_comp cmp (compress_word v1) (compress_word v2)
and compress_bool (Fp_bopt sc v) = compress_bool v