forked from CakeML/cakeml
-
Notifications
You must be signed in to change notification settings - Fork 0
/
sineProgCompScript.sml
103 lines (96 loc) · 2.68 KB
/
sineProgCompScript.sml
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
(*
Auto-generated by Daisy (https://gitlab.mpi-sws.org/AVA/daisy
*)
(* INCLUDES, do not change those *)
open exampleLib;
val _ = new_theory "sineProgComp";
val _ = translation_extends "cfSupport";
Definition theAST_pre_def:
theAST_pre = \ (x:(string, string) id).
if x = Short "x" then (((-157079632679)/(100000000000), (157079632679)/(100000000000)):real#real)
else (0,0)
End
Definition theAST_def:
theAST =
[ Dlet unknown_loc (Pvar "sine")
(Fun "x"
(FpOptimise Opt
(App (FP_bop FP_Sub)
[
(App (FP_bop FP_Add)
[
(App (FP_bop FP_Sub)
[
Var (Short "x");
(App (FP_bop FP_Div)
[
(App (FP_bop FP_Mul)
[
(App (FP_bop FP_Mul)
[
Var (Short "x");
Var (Short "x")
]);
Var (Short "x")
]);
(App FpFromWord [Lit (Word64 (4618441417868443648w:word64))])
])
]);
(App (FP_bop FP_Div)
[
(App (FP_bop FP_Mul)
[
(App (FP_bop FP_Mul)
[
(App (FP_bop FP_Mul)
[
(App (FP_bop FP_Mul)
[
Var (Short "x");
Var (Short "x")
]);
Var (Short "x")
]);
Var (Short "x")
]);
Var (Short "x")
]);
(App FpFromWord [Lit (Word64 (4638144666238189568w:word64))])
])
]);
(App (FP_bop FP_Div)
[
(App (FP_bop FP_Mul)
[
(App (FP_bop FP_Mul)
[
(App (FP_bop FP_Mul)
[
(App (FP_bop FP_Mul)
[
(App (FP_bop FP_Mul)
[
(App (FP_bop FP_Mul)
[
Var (Short "x");
Var (Short "x")
]);
Var (Short "x")
]);
Var (Short "x")
]);
Var (Short "x")
]);
Var (Short "x")
]);
Var (Short "x")
]);
(App FpFromWord [Lit (Word64 (4662263553305083904w:word64))])
])
])))]
End
Definition theErrBound_def:
theErrBound = inv (2 pow (5))
End
val x = define_benchmark theAST_def theAST_pre_def true;
val _ = export_theory()