cakeml/semantics/fpSemScript.sml at master · nikhilranade/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
(*Generated by Lem from fpSem.lem.*)
open HolKernel Parse boolLib bossLib;
open lem_pervasivesTheory libTheory machine_ieeeTheory;

val _ = numLib.prefer_num();


val _ = new_theory "fpSem"

(*
  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*)

val _ = Hol_datatype `
 fp_cmp = FP_Less | FP_LessEqual | FP_Greater | FP_GreaterEqual | FP_Equal`;

val _ = Hol_datatype `
 fp_uop = FP_Abs | FP_Neg | FP_Sqrt`;

val _ = Hol_datatype `
 fp_bop = FP_Add | FP_Sub | FP_Mul | FP_Div`;

val _ = Hol_datatype `
 fp_top =   FP_Fma`;


(*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*)

(*val fp64_abs    : word64 -> word64*)
(*val fp64_negate : word64 -> word64*)
(*val fp64_sqrt   : rounding -> word64 -> word64*)

(*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*)

(*val fp64_mul_add : rounding -> word64 -> word64 -> word64 -> word64*)

(*val roundTiesToEven : rounding*)

(*val fp_cmp : fp_cmp -> word64 -> word64 -> bool*)
val _ = Define `
 ((fp_cmp:fp_cmp -> word64 -> word64 -> bool) fop=  ((case fop of
    FP_Less => fp64_lessThan
  | FP_LessEqual => fp64_lessEqual
  | FP_Greater => fp64_greaterThan
  | FP_GreaterEqual => fp64_greaterEqual
  | FP_Equal => fp64_equal
)))`;


(*val fp_uop : fp_uop -> word64 -> word64*)
val _ = Define `
 ((fp_uop:fp_uop -> word64 -> word64) fop=  ((case fop of
    FP_Abs => fp64_abs
  | FP_Neg => fp64_negate
  | FP_Sqrt => fp64_sqrt roundTiesToEven
)))`;


(*val fp_bop : fp_bop -> word64 -> word64 -> word64*)
val _ = Define `
 ((fp_bop:fp_bop -> word64 -> word64 -> word64) fop=  ((case fop of
    FP_Add => fp64_add roundTiesToEven
  | FP_Sub => fp64_sub roundTiesToEven
  | FP_Mul => fp64_mul roundTiesToEven
  | FP_Div => fp64_div roundTiesToEven
)))`;


val _ = Define `
 ((fpfma:word64 -> word64 -> word64 -> word64) v1 v2 v3=  (fp64_mul_add roundTiesToEven v2 v3 v1))`;


(*val fp_top : fp_top -> word64 -> word64 -> word64 -> word64*)
val _ = Define `
 ((fp_top:fp_top -> word64 -> word64 -> word64 -> word64) fop=  ((case fop of
    FP_Fma => fpfma
)))`;

val _ = export_theory()