nat.jml

public Nat -> type
  | O : Nat
  | S : Nat -> Nat

public successor -> fun (n : Nat) : Nat => S n
public predecessor -> fun (S n : Nat) : Nat => n

public n + m ->
  split n, m into
  | _, O -> n
  | O, _ -> m
  | _, S m' -> S n + m' 
  end

public n - m ->
  split n, m into
  | O, _ -> O
  | _, O -> n
  | S n', S m' -> n' - m'
  end

multiply_tail_recursive ->
  fun (n : Nat) (m : Nat) (acc : Nat) : Nat =>
    split n, m into
    | O, _ -> acc
    | _, O -> acc
    | _, S m' ->
      multiply_tail_recursive n (m := m') (acc <<- n + _)
    end

public n * m -> multiply_tail_recursive n m (acc := O)

divmod_tail_recursive ->
  fun (n : Nat) (S m : Nat) (quotient : Nat) : (Nat, Nat) =>
    split n < m into
    | true -> (quotient, n)
    | false ->
      divmod_tail_recursive (n := n - m) m (quotient <<- S _)
    end

public divmod ->
  fun (n : Nat) (m : Nat) : (Nat, Nat) =>
    split m into
    | O -> (O, O)
    | S _ -> divmod_tail_recursive n m
    end

public divmod_fallible ->
  fun (n : Nat) (m : Nat) : Result (Nat, Nat) String =>
    split m into
    | O -> Error "division by zero"
    | S _ -> Ok (divmod_tail_recursive n m)
    end

public dividend / divisor ->
  first (divmod (n := dividend) (m := divisor))

public dividend % divisor ->
  second (divmod (n := dividend) (m := divisor))

power_tail_recursive ->
  fun (n : Nat) (m : Nat) (acc : Nat) : Nat =>
    split m into
    | O -> acc
    | S m' ->
      power_tail_recursive n (m := m') (acc <<- n * _)
    end

public n^m -> power_tail_recursive n m (acc := S O)

public double -> fun (n : nat) => n + n

halve_tail_recursive ->
  fun (n : Nat) (acc : Nat) : Nat =>
    split n into
    | O | S O -> acc
    | S (S n'') -> halve_tail_recursive (n := n'') (acc <<- S _)
    end

halve -> fun (n : nat) => halve_tail_recursive n (acc := O)
square -> fun (n : nat) => n * n

square_root_tail_recursive ->
  fun (remainder : Nat)
      (candidate : Nat)
      (upper_bound : Nat)
      (correction : Nat) =>
    split remainder into
    | O -> candidate
    | S remainder' ->
      split correction into
      | O ->
        square_root_tail_recursive
          (remainder := remainder')
          (candidate <<- S)
          (upper_bound := S (S upper_bound))
          (correction := S (S upper_bound))
      | S correction' ->
        square_root_tail_recursive
          (remainder := remainder')
          candidate
          upper_bound
          (correction := correction')
      end
    end

public square_root ->
  fun (n : Nat) =>
    square_root_tail_recursive
      (remainder := remainder')
      (candidate := O)
      (upper_bound := O)
      (correction := O)