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
|
/************************************************************************/
/* * The Coq Proof Assistant / The Coq Development Team */
/* v * Copyright INRIA, CNRS and contributors */
/* <O___,, * (see version control and CREDITS file for authors & dates) */
/* \VV/ **************************************************************/
/* // * This file is distributed under the terms of the */
/* * GNU Lesser General Public License Version 2.1 */
/* * (see LICENSE file for the text of the license) */
/************************************************************************/
#ifndef _COQ_FLOAT64_
#define _COQ_FLOAT64_
#include <math.h>
#define DECLARE_FREL(name, e) \
int coq_##name(double x, double y) { \
return e; \
} \
\
value coq_##name##_byte(value x, value y) { \
return coq_##name(Double_val(x), Double_val(y)); \
}
#define DECLARE_FBINOP(name, e) \
double coq_##name(double x, double y) { \
return e; \
} \
\
value coq_##name##_byte(value x, value y) { \
return caml_copy_double(coq_##name(Double_val(x), Double_val(y))); \
}
#define DECLARE_FUNOP(name, e) \
double coq_##name(double x) { \
return e; \
} \
\
value coq_##name##_byte(value x) { \
return caml_copy_double(coq_##name(Double_val(x))); \
}
DECLARE_FREL(feq, x == y)
DECLARE_FREL(flt, x < y)
DECLARE_FREL(fle, x <= y)
DECLARE_FBINOP(fmul, x * y)
DECLARE_FBINOP(fadd, x + y)
DECLARE_FBINOP(fsub, x - y)
DECLARE_FBINOP(fdiv, x / y)
DECLARE_FUNOP(fsqrt, sqrt(x))
DECLARE_FUNOP(next_up, nextafter(x, INFINITY))
DECLARE_FUNOP(next_down, nextafter(x, -INFINITY))
value coq_is_double(value x) {
return Val_long(Is_double(x));
}
#endif /* _COQ_FLOAT64_ */
|
