cakeml/unverified/lem/fpSem.lem at master · ericlp/cakeml · GitHub

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
(*
  Definitions of the floating point operations used in CakeML.
*)
open import Pervasives
open import Lib

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`

type fp_cmp = FP_Less | FP_LessEqual | FP_Greater | FP_GreaterEqual | FP_Equal
type fp_uop = FP_Abs | FP_Neg | FP_Sqrt
type fp_bop = FP_Add | FP_Sub | FP_Mul | FP_Div
type fp_top = | FP_Fma
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

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_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 : fp_cmp -> word64 -> word64 -> bool
let fp_cmp 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_uop : fp_uop -> word64 -> word64
let fp_uop fop = match fop with
  | FP_Abs -> fp64_abs
  | FP_Neg -> fp64_negate
  | FP_Sqrt -> fp64_sqrt roundTiesToEven
end

val fp_bop : fp_bop -> word64 -> word64 -> word64
let fp_bop 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 : fp_top -> word64 -> word64 -> word64 -> word64
let fp_top fop = match fop with
  | FP_Fma -> fpfma
end