|
| 1 | +#lang herbie/platform |
| 2 | + |
| 3 | +(require math/flonum) |
| 4 | + |
| 5 | +(define 64bit-move-cost 0.125) |
| 6 | +(define boolean-move-cost 0.100) |
| 7 | + |
| 8 | +(define-representation <bool> #:cost boolean-move-cost) |
| 9 | +(define-representation <binary64> #:cost 64bit-move-cost) |
| 10 | + |
| 11 | +(define-operations () <bool> |
| 12 | + [true #:spec (TRUE) #:impl (const true) #:fpcore TRUE #:cost boolean-move-cost] |
| 13 | + [false #:spec (FALSE) #:impl (const false) #:fpcore FALSE #:cost boolean-move-cost]) |
| 14 | + |
| 15 | +(define-operations ([x <bool>] [y <bool>]) <bool> |
| 16 | + [and #:spec (and x y) #:impl (lambda v (andmap values v)) #:cost boolean-move-cost] |
| 17 | + [or #:spec (or x y) #:impl (lambda v (ormap values v)) #:cost boolean-move-cost]) |
| 18 | + |
| 19 | +(define-operation (not [x <bool>]) <bool> |
| 20 | + #:spec (not x) #:impl not #:cost boolean-move-cost) |
| 21 | + |
| 22 | +(define-operation (if.py [c <bool>] [t <binary64>] [f <binary64>]) <binary64> |
| 23 | + #:spec (if c t f) #:impl if-impl |
| 24 | + #:cost boolean-move-cost #:aggregate if-cost) |
| 25 | + |
| 26 | + |
| 27 | + |
| 28 | +(define-operations ([x <binary64>] [y <binary64>]) <bool> |
| 29 | + [== #:spec (== x y) #:impl = #:cost 64bit-move-cost] |
| 30 | + [!= #:spec (!= x y) #:impl (negate =) #:cost 64bit-move-cost] |
| 31 | + [< #:spec (< x y) #:impl < #:cost 64bit-move-cost] |
| 32 | + [> #:spec (> x y) #:impl > #:cost 64bit-move-cost] |
| 33 | + [<= #:spec (<= x y) #:impl <= #:cost 64bit-move-cost] |
| 34 | + [>= #:spec (>= x y) #:impl >= #:cost 64bit-move-cost]) |
| 35 | + |
| 36 | +(define-operations () <binary64> |
| 37 | + [pi #:spec (PI) #:impl (const (flsingle pi)) #:fpcore PI #:cost 64bit-move-cost] |
| 38 | + [e #:spec (E) #:impl (const (flsingle (exp 1))) #:fpcore E #:cost 64bit-move-cost] |
| 39 | + [inf #:spec (INFINITY) #:impl (const +inf.0) #:fpcore INFINITY #:cost 64bit-move-cost] |
| 40 | + [nan #:spec (NAN) #:impl (const +nan.0) #:fpcore NAN #:cost 64bit-move-cost] |
| 41 | + [tau #:spec (* 2 (PI)) #:impl (const(* 2 pi)) #:fpcore (* 2 PI) #:cost 64bit-move-cost]) |
| 42 | + |
| 43 | +(define-operations ([x <binary64>] [y <binary64>]) <binary64> |
| 44 | + [+.py #:spec (+ x y) #:impl (compose flsingle +) #:cost 0.200] |
| 45 | + [-.py #:spec (- x y) #:impl (compose flsingle -) #:cost 0.200] |
| 46 | + [*.py #:spec (* x y) #:impl (compose flsingle *) #:cost 0.250] |
| 47 | + [/.py #:spec (/ x y) #:impl (compose flsingle /) #:cost 0.350]) |
| 48 | + |
| 49 | +(define-operations ([x <binary64>]) <binary64> |
| 50 | + [degrees.py #:spec (* x (/ (PI) 180.0)) #:impl radians->degrees #:fpcore (degrees x) #:cost 1] |
| 51 | + [radians.py #:spec (* x (/ 180.0 (PI))) #:impl degrees->radians #:fpcore (radians x) #:cost 1] |
| 52 | + [neg.py #:spec (neg x) #:impl - #:cost 0.125] |
| 53 | + [fabs.py #:spec (fabs x) #:impl (from-libm 'fabs) #:cost 1] |
| 54 | + [sin.py #:spec (sin x) #:impl (from-libm 'sin) #:cost 1] |
| 55 | + [sinh.py #:spec (sinh x) #:impl (from-libm 'sinh) #:cost 1] |
| 56 | + [asin.py #:spec (asin x) #:impl (from-libm 'asin) #:cost 1] |
| 57 | + [asinh.py #:spec (asinh x) #:impl (from-libm 'asinh) #:cost 1] |
| 58 | + [cos.py #:spec (cos x) #:impl (from-libm 'cos) #:cost 1] |
| 59 | + [cosh.py #:spec (cosh x) #:impl (from-libm 'cosh) #:cost 1] |
| 60 | + [acos.py #:spec (acos x) #:impl (from-libm 'acos) #:cost 1] |
| 61 | + [acosh.py #:spec (acosh x) #:impl (from-libm 'acosh) #:cost 1] |
| 62 | + [tan.py #:spec (tan x) #:impl (from-libm 'tan) #:cost 1] |
| 63 | + [atan.py #:spec (atan x) #:impl (from-libm 'atan) #:cost 1] |
| 64 | + [atanh.py #:spec (atanh x) #:impl (from-libm 'atanh) #:cost 1] |
| 65 | + [tanh.py #:spec (tanh x) #:impl (from-libm 'tanh) #:cost 1] |
| 66 | + [sqrt.py #:spec (sqrt x) #:impl (from-libm 'sqrt) #:cost 1] |
| 67 | + [cbrt.py #:spec (cbrt x) #:impl (from-libm 'cbrt) #:cost 1] |
| 68 | + [ceil.py #:spec (ceil x) #:impl (from-libm 'ceil) #:cost 1] |
| 69 | + [floor.py #:spec (floor x) #:impl (from-libm 'floor) #:cost 1] |
| 70 | + [erf.py #:spec (erf x) #:impl (from-libm 'erf) #:cost 1] |
| 71 | + [exp.py #:spec (exp x) #:impl (from-libm 'exp) #:cost 1] |
| 72 | + [exp2.py #:spec (exp2 x) #:impl (from-libm 'exp2) #:cost 1] |
| 73 | + [gamma.py #:spec (tgamma x) #:impl (from-libm 'tgamma) #:cost 1] |
| 74 | + [lgamma.py #:spec (lgamma x) #:impl (from-libm 'lgamma) #:cost 1] |
| 75 | + [log.1var #:spec (log x) #:impl (from-libm 'log) #:cost 1] |
| 76 | + [log10.py #:spec (log10 x) #:impl (from-libm 'log10) #:cost 1] |
| 77 | + [log2.py #:spec (log2 x) #:impl (from-libm 'log2) #:cost 1] |
| 78 | + [rint.py #:spec (rint x) #:impl (from-libm 'rint) #:cost 1] |
| 79 | + [round.py #:spec (round x) #:impl (from-libm 'round) #:cost 1] |
| 80 | + [trunc.py #:spec (trunc x) #:impl (from-libm 'trunc) #:cost 1]) |
| 81 | + |
| 82 | +(define-operations ([x <binary64>]) <binary64> |
| 83 | + [erfc.py #:spec (- 1 (erf x)) #:impl (from-libm 'erfc) #:fpcore (erfc x) #:cost 1] |
| 84 | + [expm1.py #:spec (- (exp x) 1) #:impl (from-libm 'expm1) #:fpcore (expm1 x) #:cost 1] |
| 85 | + [log1p.py #:spec (log (+ 1 x)) #:impl (from-libm 'log1p) #:fpcore (log1p x) #:cost 1]) |
| 86 | + |
| 87 | +(define-operations ([x <binary64>] [y <binary64>]) <binary64> |
| 88 | + [pow.py #:spec (pow x y) #:impl (from-libm 'pow) #:cost 1] |
| 89 | + [atan2.py #:spec (atan2 x y) #:impl (from-libm 'atan2) #:cost 1] |
| 90 | + [copysign.py #:spec (copysign x y) #:impl (from-libm 'copysign) #:cost 1] |
| 91 | + [fdim.py #:spec (fdim x y) #:impl (from-libm 'fdim) #:cost 1] |
| 92 | + [fmax.py #:spec (fmax x y) #:impl (from-libm 'fmax) #:cost 1] |
| 93 | + [fmin.py #:spec (fmin x y) #:impl (from-libm 'fmin) #:cost 1] |
| 94 | + [fmod.py #:spec (fmod x y) #:impl (from-libm 'fmod) #:cost 1] |
| 95 | + [remainder.py #:spec (remainder x y) #:impl (from-libm 'remainder) #:cost 1]) |
| 96 | + |
| 97 | +(define-operations ([x <binary64>] [y <binary64>] [w <binary64>]) <binary64> |
| 98 | + [fsum.3var #:spec (+ (+ x y) w) #:impl (curry apply flsum) #:fpcore (fsum x y w) #:cost 1] |
| 99 | + [prod.3var #:spec (* (* x y) w) #:impl (from-rival) #:fpcore (prod x y w) #:cost 1]) |
| 100 | + |
| 101 | +(define-operations ([x <binary64>] [y <binary64>] [w <binary64>] [z <binary64>]) <binary64> |
| 102 | + [fsum.4var #:spec (+ (+ (+ x y) z) w) #:impl (curry apply flsum) #:fpcore (fsum x y w z) #:cost 1] |
| 103 | + [prod.4var #:spec (* (* (* x y) w) z) #:impl (from-rival) #:fpcore (prod x y w z) #:cost 1]) |
| 104 | + |
| 105 | +(define-operation (dist.2D [x <binary64>] [y <binary64>] [z <binary64>] [w <binary64>]) <binary64> |
| 106 | + #:spec (sqrt (+ (pow (- y x) 2) (pow (- w z) 2))) #:impl (from-rival) |
| 107 | + #:fpcore (dist x y z w) #:cost 1) |
| 108 | + |
| 109 | +(define-operation (dist.3D [x <binary64>] [y <binary64>] [z <binary64>] [w <binary64>] [u <binary64>] [v <binary64>]) <binary64> |
| 110 | + #:spec (sqrt (+ (+ (pow (- y x) 2) (pow (- w z) 2)) (pow (- v u) 2))) #:impl (from-rival) |
| 111 | + #:fpcore (dist x y z w u v) #:cost 1) |
| 112 | + |
| 113 | +(define-operation (sumprod.2D [x <binary64>] [y <binary64>] [z <binary64>] [w <binary64>]) <binary64> |
| 114 | + #:spec (+ (* x y) (* z w)) #:impl (from-rival) |
| 115 | + #:fpcore (sumprod x y z w) #:cost 1) |
| 116 | + |
| 117 | +(define-operation (sumprod.3D [x <binary64>] [y <binary64>] [z <binary64>] [w <binary64>] [u <binary64>] [v <binary64>]) <binary64> |
| 118 | + #:spec (+ (+ (* x y) (* z w)) (* u v)) #:impl (from-rival) |
| 119 | + #:fpcore (sumprod x y z w u v) #:cost 1) |
| 120 | + |
| 121 | +(define-operation (hypot.2D [x <binary64>] [y <binary64>]) <binary64> |
| 122 | + #:spec (sqrt (+ (* x x) (* y y))) #:impl (from-libm 'hypot) |
| 123 | + #:fpcore (hypot x y) #:cost 1) |
| 124 | + |
| 125 | +(define-operation (hypot.3D [x <binary64>] [y <binary64>] [z <binary64>]) <binary64> |
| 126 | + #:spec (sqrt (+ (+ (* x x) (* y y)) (* z z))) #:impl (from-rival) |
| 127 | + #:fpcore (hypot x y z) #:cost 1) |
| 128 | + |
| 129 | +(define-operation (fma.py [x <binary64>] [y <binary64>] [z <binary64>]) <binary64> |
| 130 | + #:spec (+ (* x y) z) #:impl (from-libm 'fma) |
| 131 | + #:fpcore (fma x y z) #:cost 1) |
0 commit comments