### Be careful with the pipe operator in Reason

The evaluation order may be different from the left-to-right order if the pipe operator is present.

The generated code for this example is similar to the following code:

``````Caml_obj.caml_equal(Caml_array.caml_array_get(a.sort(), 0), Caml_array.caml_array_get(\$\$Array.copy(a), 0));
``````
``let f = (a: array(int)): int => a[0]``

### NASM: Get Max of two integers

Code
Diff
• ``````section .text
global max ; declare max function
max:                ; long max(long a, long b)
mov rax, rsi      ; default to b
cmp rax, rdi
cmovl rax, rdi
ret``````
•  1 1 section .text 2 2 global max ; declare max function 3 3 max: ; long max(long a, long b) 4 4 mov rax, rsi ; default to b 5 − sub rsi, rdi 6 − sar rsi, 63 ; get sign 7 − xor rdi, rax 8 − and rsi, rdi 9 − xor rax, rsi ; rax is now the max 10 − xor rsi, rax ; rsi is reset - not sure if this is important 11 − xor rdi, rsi ; rdi is reset - not sure if this is important 12 − ret ; i wasted three sheets of paper trying to figure this solution out 5 + cmp rax, rdi 6 + cmovl rax, rdi 7 + ret

### Stream Based n-choose-k Method

Algorithms
Arrays
Mathematics
Numbers
Code
Diff
• ``````import java.util.stream.IntStream;

public class ArrayFactorial{
public static int factorial(int n, int k) {
return IntStream.rangeClosed(1, Math.min(k, n - k))
.reduce(1, (r, i) -> r * (n - i + 1) / i);
}
}``````
• 1import java. math. BigInteger;
2import java. util. stream. *;
1+import java.util.stream.IntStream;
33
44 public class ArrayFactorial{
5 public static int factorial( int n, int k){
6 int lower= Math. min( k, n- k);
7 int higher= Math. max( k, n- k);
8 return IntStream. range( 2, lower+ 1)
9 . mapToObj( BigInteger:: valueOf)
4+ public static int factorial(int n, int k) {
5+ return IntStream.rangeClosed(1, Math.min(k, n - k))
6+ .reduce(1, (r, i) -> r * (n - i + 1) / i);
1616 }
1717 }

### Return Even Whatever You've Been Given

Code
Diff
• ``e=lambda n:n&-2``
•  1 − def e(n): return n-n%2 1 + e=lambda n:n&-2
Failed Tests

### Lean 3.11 is slow

``````import analysis.special_functions.trigonometric

#check complex.continuous_cos``````

### Code extraction tests

Large factorials with `Num`.

### Code extraction tests

``````Fixpoint factorial (n : nat) :=
match n with
| O => 1
| S n' => n * factorial n'
end.``````

### Divide by 3 without division operation

Code
Diff
• ``dividedByThree=n=> (n * -1431655765 + 715827882 >>> 0) < 1431655765;``
•  1 − // i assume this is an allowed use of "/" :) 2 − dividedByThree=n=>/^-?0*(0*1(01*0)*1)*0*\$/.test(n.toString(2)) 1 + dividedByThree=n=> (n * -1431655765 + 715827882 >>> 0) < 1431655765;

### Non-structural well-founded recursion using Program Fixpoint

Fundamentals
Theorem Proving

`interleave` using `Equations`.

Code
Diff
• ``````From Coq Require Import Lists.List omega.Omega.
Import ListNotations.

From Equations Require Import Equations.

Equations interleave {A} (l1 l2 : list A) : list A by wf (length (l1 ++ l2)) lt :=
interleave [] l2 := l2;
interleave (x :: xs) l2 := x :: interleave l2 xs.
Next Obligation. rewrite !app_length; omega. Qed.

Example test_interleave1:
interleave [1;2;3] [4;5;6] = [1;4;2;5;3;6].
Proof. reflexivity. Qed.
Example test_interleave2:
interleave [1] [4;5;6] = [1;4;5;6].
Proof. reflexivity. Qed.
Example test_interleave3:
interleave [1;2;3] [4] = [1;4;2;3].
Proof. reflexivity. Qed.
Example test_interleave4:
interleave [] [20;30] = [20;30].
Proof. reflexivity. Qed.``````
• 11 From Coq Require Import Lists.List omega.Omega.
22 Import ListNotations.
33
4Fail Fixpoint interleave {A} (l1 l2 : list A) : list A :=
5 match l1 with
6 | [] => l2
7 | x :: xs => x :: interleave l2 xs
8 end.
4+From Equations Require Import Equations.
99
10Require Import Recdef.
11
12Fail Function interleave {A} (l1 l2 : list A) {measure length (l1 ++ l2)} : list A :=
13 match l1 with
14 | [] => l2
6+Equations interleave {A} (l1 l2 : list A) : list A by wf (length (l1 ++ l2)) lt :=
7+interleave [] l2 := l2;
8+interleave (x :: xs) l2 := x :: interleave l2 xs.
9+Next Obligation. rewrite !app_length; omega. Qed.

### JS BigInt in Reason

Code
Diff
• ``````open Preloaded;

let fib = (n) => {
let rec fib_aux = (n, a, b) =>
if (n <= 0) { a; }
else { fib_aux(n - 1, b, a +@ b); }
fib_aux(n, big_int_of_int(0), big_int_of_int(1))
|> string_of_big_int;
};

let fib64 = (n) => {
// Open Int64 locally
open Int64;
let rec fib_aux = (n, a, b) =>
if (n <= 0) { a; }
else { fib_aux(n - 1, b, add(a, b)); }
fib_aux(n, zero, one)
|> to_string;
};
``````
•  1 1 open Preloaded; 2 2 3 3 let fib = (n) => { 4 4 let rec fib_aux = (n, a, b) => 5 5 if (n <= 0) { a; } 6 6 else { fib_aux(n - 1, b, a +@ b); } 7 7 fib_aux(n, big_int_of_int(0), big_int_of_int(1)) 8 8 |> string_of_big_int; 9 9 }; 10 10 11 + let fib64 = (n) => { 12 + // Open Int64 locally 13 + open Int64; 14 + let rec fib_aux = (n, a, b) => 15 + if (n <= 0) { a; } 16 + else { fib_aux(n - 1, b, add(a, b)); } 17 + fib_aux(n, zero, one) 18 + |> to_string; 19 + };

### JS BigInt in Reason

``````open Preloaded;

let fib = (n) => {
let rec fib_aux = (n, a, b) =>
if (n <= 0) { a; }
else { fib_aux(n - 1, b, a +@ b); }
fib_aux(n, big_int_of_int(0), big_int_of_int(1))
|> string_of_big_int;
};``````