diff options
| author | Pierre Roux | 2018-08-28 18:56:07 +0200 |
|---|---|---|
| committer | Pierre Roux | 2019-11-01 10:20:35 +0100 |
| commit | d18b928154a48ff8d90aaff69eca7d6eb3dfa0ab (patch) | |
| tree | 9cc9b39b16849ed839f4adf7b19e3d3291f7dd98 /kernel/byterun | |
| parent | 79605dabb10e889ae998bf72c8483f095277e693 (diff) | |
Implement classify on primitive float
Diffstat (limited to 'kernel/byterun')
| -rw-r--r-- | kernel/byterun/coq_fix_code.c | 1 | ||||
| -rw-r--r-- | kernel/byterun/coq_interp.c | 25 | ||||
| -rw-r--r-- | kernel/byterun/coq_values.h | 9 |
3 files changed, 35 insertions, 0 deletions
diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index bca2cc3bd9..fb39ca8358 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -65,6 +65,7 @@ void init_arity () { arity[CHECKEQINT63]=arity[CHECKLTINT63]=arity[CHECKLEINT63]= arity[CHECKCOMPAREINT63]=arity[CHECKHEAD0INT63]=arity[CHECKTAIL0INT63]= arity[CHECKOPPFLOAT]=arity[CHECKABSFLOAT]=arity[CHECKCOMPAREFLOAT]= + arity[CHECKCLASSIFYFLOAT]= arity[CHECKADDFLOAT]=arity[CHECKSUBFLOAT]=arity[CHECKMULFLOAT]= arity[CHECKDIVFLOAT]=arity[CHECKSQRTFLOAT]= arity[CHECKFLOATOFINT63]=arity[CHECKFLOATNORMFRMANTISSA]= diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 74edd79872..b862480fda 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -1565,6 +1565,31 @@ value coq_interprete Next; } + Instruct (CHECKCLASSIFYFLOAT) { + double x; + print_instr("CHECKCLASSIFYFLOAT"); + CheckFloat1(); + x = Double_val(accu); + switch (fpclassify(x)) { + case FP_NORMAL: + accu = signbit(x) ? coq_NNormal : coq_PNormal; + break; + case FP_SUBNORMAL: + accu = signbit(x) ? coq_NSubn : coq_PSubn; + break; + case FP_ZERO: + accu = signbit(x) ? coq_NZero : coq_PZero; + break; + case FP_INFINITE: + accu = signbit(x) ? coq_NInf : coq_PInf; + break; + default: /* FP_NAN */ + accu = coq_NaN; + break; + } + Next; + } + Instruct (CHECKADDFLOAT) { print_instr("CHECKADDFLOAT"); CheckFloat2(); diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h index c79a8f1b4f..b027673ac7 100644 --- a/kernel/byterun/coq_values.h +++ b/kernel/byterun/coq_values.h @@ -46,6 +46,15 @@ #define coq_FLt Val_int(1) #define coq_FGt Val_int(2) #define coq_FNotComparable Val_int(3) +#define coq_PNormal Val_int(0) +#define coq_NNormal Val_int(1) +#define coq_PSubn Val_int(2) +#define coq_NSubn Val_int(3) +#define coq_PZero Val_int(4) +#define coq_NZero Val_int(5) +#define coq_PInf Val_int(6) +#define coq_NInf Val_int(7) +#define coq_NaN Val_int(8) #define FLOAT_EXP_SHIFT (2101) /* 2*emax + prec */ |