-
Notifications
You must be signed in to change notification settings - Fork 85
/
Copy pathkepler1ProgCompScript.sml
129 lines (122 loc) · 3.72 KB
/
kepler1ProgCompScript.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
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
(*
Auto-generated by Daisy (https://gitlab.mpi-sws.org/AVA/daisy
*)
(* INCLUDES, do not change those *)
open exampleLib;
val _ = new_theory "kepler1ProgComp";
val _ = translation_extends "cfSupport";
Definition theAST_pre_def:
theAST_pre = \ (x:(string, string) id).
if x = Short "x1" then (((4)/(1), (159)/(25)):real#real)
else if x = Short "x2" then (((4)/(1), (159)/(25)):real#real)
else if x = Short "x3" then (((4)/(1), (159)/(25)):real#real)
else if x = Short "x4" then (((4)/(1), (159)/(25)):real#real)
else (0,0)
End
Definition theAST_def:
theAST =
[ Dlet unknown_loc (Pvar "kepler1")
(Fun "x1"(Fun "x2"(Fun "x3"(Fun "x4"
(FpOptimise Opt
(App (FP_bop FP_Sub)
[
(App (FP_bop FP_Sub)
[
(App (FP_bop FP_Sub)
[
(App (FP_bop FP_Sub)
[
(App (FP_bop FP_Add)
[
(App (FP_bop FP_Add)
[
(App (FP_bop FP_Mul)
[
(App (FP_bop FP_Mul)
[
Var (Short "x1");
Var (Short "x4")
]);
(App (FP_bop FP_Sub)
[
(App (FP_bop FP_Add)
[
(App (FP_bop FP_Add)
[
(App (FP_uop FP_Neg)
[
Var (Short "x1")
]);
Var (Short "x2")
]);
Var (Short "x3")
]);
Var (Short "x4")
])
]);
(App (FP_bop FP_Mul)
[
Var (Short "x2");
(App (FP_bop FP_Add)
[
(App (FP_bop FP_Add)
[
(App (FP_bop FP_Sub)
[
Var (Short "x1");
Var (Short "x2")
]);
Var (Short "x3")
]);
Var (Short "x4")
])
])
]);
(App (FP_bop FP_Mul)
[
Var (Short "x3");
(App (FP_bop FP_Add)
[
(App (FP_bop FP_Sub)
[
(App (FP_bop FP_Add)
[
Var (Short "x1");
Var (Short "x2")
]);
Var (Short "x3")
]);
Var (Short "x4")
])
])
]);
(App (FP_bop FP_Mul)
[
(App (FP_bop FP_Mul)
[
Var (Short "x2");
Var (Short "x3")
]);
Var (Short "x4")
])
]);
(App (FP_bop FP_Mul)
[
Var (Short "x1");
Var (Short "x3")
])
]);
(App (FP_bop FP_Mul)
[
Var (Short "x1");
Var (Short "x2")
])
]);
Var (Short "x4")
]))))))]
End
Definition theErrBound_def:
theErrBound = inv (2 pow (5))
End
val x = define_benchmark theAST_def theAST_pre_def true;
val _ = export_theory()