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]
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
  • 11 section .text
    22 global max ; declare max function
    33 max: ; long max(long a, long b)
    44 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
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 }
Code
Diff
  • e=lambda n:n&-2
  • 1def e(n): return n-n%2
    1+e=lambda n:n&-2
import analysis.special_functions.trigonometric

#check complex.continuous_cos

Large factorials with Num.

Fixpoint factorial (n : nat) :=
  match n with
  | O => 1
  | S n' => n * factorial n'
  end.
Code
Diff
  • dividedByThree=n=> (n * -1431655765 + 715827882 >>> 0) < 1431655765;
  • 1// i assume this is an allowed use of "/" :)
    2dividedByThree=n=>/^-?0*(0*1(01*0)*1)*0*$/.test(n.toString(2))
    1+dividedByThree=n=> (n * -1431655765 + 715827882 >>> 0) < 1431655765;
Advanced Language Features
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.
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;
    };
    
  • 11 open Preloaded;
    22
    33 let fib = (n) => {
    44 let rec fib_aux = (n, a, b) =>
    55 if (n <= 0) { a; }
    66 else { fib_aux(n - 1, b, a +@ b); }
    77 fib_aux(n, big_int_of_int(0), big_int_of_int(1))
    88 |> string_of_big_int;
    99 };
    1010
    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+};
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;
};