Skip to content

Commit 13acf3d

Browse files
authored
Merge pull request #7 from Zite0/main
Replace Cartesian Product Syntax
2 parents 20c3cc9 + 5c9bb3e commit 13acf3d

35 files changed

+2131
-2126
lines changed

doc/README.md

Lines changed: 26 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -41,11 +41,11 @@ FPTaylor requires the [OCaml Num library](https://github.com/ocaml/num) which ca
4141
```
4242
opam install num
4343
```
44-
Now, in the directory `NumFuzz/examples/FPTaylor`, extract FPTaylor to the directory `FPTaylor-9.4.0` by running the command
44+
Now, in the directory `NumFuzz/examples/FPTaylor`, extract FPTaylor to the directory `FPTaylor-0.9.4` by running the command
4545
```
4646
tar -xzf v0.9.4.tar.gz
4747
```
48-
In the directory `FPTaylor-9.4.0` run
48+
In the directory `FPTaylor-0.9.4` run
4949
```
5050
make all
5151
```
@@ -249,7 +249,7 @@ v, w ::= VALUES
249249
() value of unit type
250250
k in R constants (reals > 0)
251251
(v,w) tensor pairs
252-
(|v,w|) cartesian pairs
252+
<v,w> cartesian pairs
253253
inl v injection into sum
254254
inr v injection into sum
255255
fun (x:T) {e} ordinary function
@@ -266,8 +266,8 @@ e, f ::= EXPRESSIONS
266266
fst v cartesian pair destructor
267267
snd v cartesian pair destructor
268268
let (x,y) = v; e tensor destructor
269-
case v {inl x => e | inr x => f} case analysis
270-
if v then {e} else {f} conditional (case sugar)
269+
case v {inl x => e | inr x => f} case analysis
270+
if v then {e} else {f} conditional (case sugar)
271271
let [x] = v; e co-monadic sequencing
272272
let x = v; e monadic sequencing
273273
x = e; f pure sequencing
@@ -337,47 +337,50 @@ followed by the input function to be applied to each element in the input tuple.
337337

338338
### Arithmetic Operations with Rounding
339339

340-
Arithmetic operations that perform rounding can be built from primitive operations. One example is `addfp`, which adds two numbers and rounds the result:
340+
Arithmetic operations that perform rounding can be built from primitive operations. One example is `addfp64`, which adds two numbers and rounds the result to the nearest 64-bit floating point number:
341341

342342
```ocaml
343-
function addfp (xy: <num, num>)
343+
function addfp_64 (xy: <num, num>)
344344
{
345345
s = add xy;
346-
rnd s
346+
rnd_64 s
347347
}
348348
```
349349

350-
Several operations that perform rounding are included in the directory `NumFuzz/examples/NumFuzz/float_ops`; we list them here with their type signatures.
350+
Several operations that perform rounding are included in the directory `NumFuzz/examples/NumFuzz/float_ops`; we list the
351+
64-bit ones here with their type signatures.
351352

352-
1. Addition `addfp: (num × num) -o M[eps64_up]num`
353-
2. Multiplication `mulfp: (num ⊗ num) -o M[eps64_up]num`
354-
3. Division `divfp: (num ⊗ num) -o M[eps64_up]num`
355-
4. Square root `sqrtfp: ![0.5]num -o M[eps64_up]num`
356-
5. Fused multiply-add `FMA: num -o num -o num -o M[eps64_up]num`
357-
6. Multiply-add `MA: num -o num -o num -o M[eps64_up]num`
353+
1. Addition `addfp64: (num × num) -o M[eps64_up]num`
354+
2. Multiplication `mulfp64: (num ⊗ num) -o M[eps64_up]num`
355+
3. Division `divfp64: (num ⊗ num) -o M[eps64_up]num`
356+
4. Square root `sqrtfp64: ![0.5]num -o M[eps64_up]num`
357+
5. Fused multiply-add `FMA64: num -o num -o num -o M[eps64_up]num`
358+
6. Multiply-add `MA64: num -o num -o num -o M[eps64_up]num`
358359

359360
These operations can be used in NumFuzz programs using an include statement; e.g.,
360361
```
361-
#include PATH/float_ops/addfp.fz
362+
#include PATH/float_ops/addfp64.fz
362363
```
363-
where `PATH` is the path relative to the directory of your program.
364+
where `PATH` is the path relative to the directory of your program. Operations
365+
using 16, and 32 bit floating-point numbers are also available. For example, `addfp32`
366+
is the 32-bit addition operator.
364367

365368
### A Simple Benchmark
366369

367370
As an example, let us consider the benchmark `one_by_sqrtxx`, where we are tasked with computing a relative error bound for the expression $1/\sqrt{x^2}$. We can use NumFuzz to derive a bound using the following program.
368371

369372
```ocaml
370-
1. #include "float_ops/mulfp.fz"
371-
2. #include "float_ops/divfp.fz"
372-
3. #include "float_ops/sqrtfp.fz"
373+
1. #include "float_ops/mulfp64.fz"
374+
2. #include "float_ops/divfp64.fz"
375+
3. #include "float_ops/sqrtfp64.fz"
373376
4.
374377
5. function one_by_sqrtxx (x : num)
375378
6. {
376-
7. sz = mulfp (x,x);
379+
7. sz = mulfp64 (x,x);
377380
8. let z = sz;
378-
9. sy = sqrtfp ([z{0.5}]);
381+
9. sy = sqrtfp64 ([z{0.5}]);
379382
10. let y = sy;
380-
11. divfp (1.0,y)
383+
11. divfp64 (1.0,y)
381384
12. }
382385
13.
383386
14. one_by_sqrtxx

doc/syntax.txt

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@ v, w ::= VALUES
1919
() value of unit type
2020
k in R constants (reals > 0)
2121
(v,w) tensor pairs
22-
(|v,w|) cartesian pairs
22+
<v,w> cartesian pairs
2323
inl v injection into sum
2424
inr v injection into sum
2525
fun (x:T) {e} ordinary function

examples/NumFuzz/float_ops/fma16.fz

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,6 @@ function FMA16
22
(x : num) (y : num) (z : num) : M[eps16_up]num
33
{
44
a = mul (x,y);
5-
b = add (|a,z|);
5+
b = add <a,z>;
66
rnd16 b
77
}

examples/NumFuzz/float_ops/fma32.fz

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,6 @@ function FMA32
22
(x : num) (y : num) (z : num) : M[eps32_up]num
33
{
44
a = mul (x,y);
5-
b = add (|a,z|);
5+
b = add <a,z>;
66
rnd32 b
77
}

examples/NumFuzz/float_ops/fma64.fz

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,6 @@ function FMA64
22
(x : num) (y : num) (z : num) : M[eps64_up]num
33
{
44
a = mul (x,y);
5-
b = add (|a,z|);
5+
b = add <a,z>;
66
rnd64 b
77
}

examples/NumFuzz/float_ops/ma64.fz

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,7 @@
1+
#include "addfp64.fz"
2+
#include "mulfp64.fz"
13
function MA64 (x : num) (y : num) (z : num) : M[4.441e-16]num {
24
s = mulfp64 (x,y);
35
let a = s;
4-
addfp64 (|a,z|)
5-
}
6+
addfp64 <a,z>
7+
}

examples/NumFuzz/hypot.fz

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ function hypot
1010
let x2 = s1;
1111
s2 = mulfp64(y,y);
1212
let y2 = s2;
13-
s3 = addfp64(|x2,y2|);
13+
s3 = addfp64<x2,y2|);
1414
let y3 = s3;
1515
sqrtfp64 [y3{0.5}]
1616
}

examples/NumFuzz/i4.fz

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ function i4
99
s1 = mulfp64(y,y);
1010
let s2 = s1;
1111
let [x] = x';
12-
s3 = addfp64 (|x, s2|);
12+
s3 = addfp64 <x, s2>;
1313
let s4 = s3;
1414
sqrtfp64 [s4{0.5}]
1515
}

examples/NumFuzz/large_benchmarks/Estrin10.fz

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -31,15 +31,15 @@ function Estrin10
3131
let t7' = t7;
3232
let t9' = t9;
3333

34-
z0 = addfp64(|a0,t1'|);
34+
z0 = addfp64<a0,t1'>;
3535
let z0' = z0;
36-
z2 = addfp64(|a2,t3'|);
36+
z2 = addfp64<a2,t3'>;
3737
let z2' = z2;
38-
z4 = addfp64(|a4,t5'|);
38+
z4 = addfp64<a4,t5'>;
3939
let z4' = z4;
40-
z6 = addfp64(|a6,t7'|);
40+
z6 = addfp64<a6,t7'>;
4141
let z6' = z6;
42-
z8 = addfp64(|a8,t9'|);
42+
z8 = addfp64<a8,t9'>;
4343
let z8' = z8;
4444

4545
p2 = mulfp64(x,x);
@@ -57,11 +57,11 @@ function Estrin10
5757
s2 = mulfp64(a10,p10');
5858
let s2' = s2;
5959

60-
u0 = addfp64(|z0',s0'|);
60+
u0 = addfp64<z0',s0'>;
6161
let u0' = u0;
62-
u1 = addfp64(|z4',s1'|);
62+
u1 = addfp64<z4',s1'>;
6363
let u1' = u1;
64-
u2 = addfp64(|z8',s2'|);
64+
u2 = addfp64<z8',s2'>;
6565
let u2' = u2;
6666

6767
r4 = pow4fp [x{4.0}];
@@ -71,13 +71,13 @@ function Estrin10
7171

7272
v00 = mulfp64(u1',r4');
7373
let v00' = v00;
74-
v0 = addfp64(|u0',v00'|);
74+
v0 = addfp64<u0',v00'>;
7575
let v0' = v0;
7676

7777
v1 = mulfp64(u2',r8');
7878
let v1' = v1;
7979

80-
addfp64(|v0',v1'|)
80+
addfp64<v0',v1'>
8181
}
8282

8383
Estrin10

examples/NumFuzz/large_benchmarks/dotprods/dotprod128.fz

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -267,7 +267,7 @@ let a125 = a125';
267267
let a126 = a126';
268268
let a127 = a127';
269269
v1 = (a0,(a1,(a2,(a3,(a4,(a5,(a6,(a7,(a8,(a9,(a10,(a11,(a12,(a13,(a14,(a15,(a16,(a17,(a18,(a19,(a20,(a21,(a22,(a23,(a24,(a25,(a26,(a27,(a28,(a29,(a30,(a31,(a32,(a33,(a34,(a35,(a36,(a37,(a38,(a39,(a40,(a41,(a42,(a43,(a44,(a45,(a46,(a47,(a48,(a49,(a50,(a51,(a52,(a53,(a54,(a55,(a56,(a57,(a58,(a59,(a60,(a61,(a62,(a63,(a64,(a65,(a66,(a67,(a68,(a69,(a70,(a71,(a72,(a73,(a74,(a75,(a76,(a77,(a78,(a79,(a80,(a81,(a82,(a83,(a84,(a85,(a86,(a87,(a88,(a89,(a90,(a91,(a92,(a93,(a94,(a95,(a96,(a97,(a98,(a99,(a100,(a101,(a102,(a103,(a104,(a105,(a106,(a107,(a108,(a109,(a110,(a111,(a112,(a113,(a114,(a115,(a116,(a117,(a118,(a119,(a120,(a121,(a122,(a123,(a124,(a125,(a126,a127)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))));
270-
g = fun (x: num) {fun (y: num) {addfp64 (|x,y|)}};
270+
g = fun (x: num) {fun (y: num) {addfp64 <x,y>}};
271271
fold128 v1 [g{127.0}]
272272
}
273273

0 commit comments

Comments
 (0)