Ad
monadius

COBOL: Multiple nested procedures

identification division.
       program-id. solution.

       data division.
       linkage section.
       01 n   pic 9.
       01 r   pic 9.
       procedure division using n r.
          display 'solution'
      * 'nested2' cannot be called here
          call 'nested2' 
            on exception display 'cannot call nested2'
          end-call
          move n to r
          goback.
       end program solution.
monadius

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]
monadiusvs.深紅心

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
    • section .text
    • global max ; declare max function
    • max: ; long max(long a, long b)
    • mov rax, rsi ; default to b
    • sub rsi, rdi
    • sar rsi, 63 ; get sign
    • xor rdi, rax
    • and rsi, rdi
    • xor rax, rsi ; rax is now the max
    • xor rsi, rax ; rsi is reset - not sure if this is important
    • xor rdi, rsi ; rdi is reset - not sure if this is important
    • ret ; i wasted three sheets of paper trying to figure this solution out
    • cmp rax, rdi
    • cmovl rax, rdi
    • ret
monadiusvs.深紅心

Stream Based n-choose-k Method

Algorithms
Logic
Arrays
Data Types
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);
    }
}
    • import java. math. BigInteger;
    • import java. util. stream. *;
    • import java.util.stream.IntStream;
    • public class ArrayFactorial{
    • public static int factorial( int n, int k){
    • int lower= Math. min( k, n- k);
    • int higher= Math. max( k, n- k);
    • return IntStream. range( 2, lower+ 1)
    • . mapToObj( BigInteger:: valueOf)
    • . reduce
    • ( IntStream. range( higher+ 1, n+ 1)
    • . mapToObj( BigInteger:: valueOf)
    • . reduce( BigInteger. ONE, ( a, b)-> a. multiply( b))
    • , ( a, b) -> a. divide( b))
    • . intValue( );
    • 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);
    • }
    • }
monadiusvs.ilya_plotnikov

Return Even Whatever You've Been Given

Code
Diff
  • e=lambda n:n&-2
    • def e(n): return n-n%2
    • e=lambda n:n&-2
monadiusFailed Tests

Lean 3.11 is slow

import analysis.special_functions.trigonometric

#check complex.continuous_cos
monadiusvs.monadius

Code extraction tests

Large factorials with Num.

monadius

Code extraction tests

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

Divide by 3 without division operation

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

Non-structural well-founded recursion using Program Fixpoint

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.
    • From Coq Require Import Lists.List omega.Omega.
    • Import ListNotations.
    • Fail Fixpoint interleave {A} (l1 l2 : list A) : list A :=
    • match l1 with
    • | [] => l2
    • | x :: xs => x :: interleave l2 xs
    • end.
    • From Equations Require Import Equations.
    • Require Import Recdef.
    • Fail Function interleave {A} (l1 l2 : list A) {measure length (l1 ++ l2)} : list A :=
    • match l1 with
    • | [] => l2
    • | x :: xs => x :: interleave l2 xs
    • end.
    • From Coq Require Import Program.Wf.
    • Program Fixpoint interleave {A} (l1 l2 : list A) {measure (length (l1 ++ l2))} : list A :=
    • match l1 with
    • | [] => l2
    • | x :: xs => x :: interleave l2 xs
    • end.
    • Fail Compute (interleave [1;2;3] [4;5;6]).
    • Next Obligation.
    • simpl.
    • repeat rewrite app_length.
    • omega.
    • Qed.
    • Compute (interleave [1;2;3] [4;5;6]).
    • 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.
monadiusvs.monadius

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;
};
    • 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;
    • };
monadius

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;
};