// Binary search
module ck/binsearchck/binsearch

import std/core/undivstd/core/undiv
import std/num/float64std/num/float64

// Binary search on the interval of integers between `ok` and `ng`.
// If `ng` < `ok`, the result is the smallest integer satisfying `p`.
// Otherwise, the result is the largest integer satisfying `p`.
// `p` must be monotone such that `p(ok)` = `True` and `p(ng)` = `False`.
pub fun binsearchck/binsearch/binsearch: forall<e> (ok : int, ng : int, p : (int) -> e bool) -> e int(okok: int: intstd/core/types/int: V, ngng: int: intstd/core/types/int: V, pp: (int) -> $18 bool: intstd/core/types/int: V -> ee: E boolstd/core/types/bool: V)result: -> 124 int: ee: E intstd/core/types/int: V
  if absstd/core/int/abs: (i : int) -> $18 int(okok: int -std/core/int/(-): (x : int, y : int) -> $18 int ngng: int) <=std/core/int/(<=): (x : int, y : int) -> $18 bool 1literal: int
dec  = 1
hex8 = 0x01
bit8 = 0b00000001 then returnreturn: int okok: int
  val mm: int = (okok: int +std/core/int/(+): (x : int, y : int) -> $18 int ngng: int) /std/core/int/(/): (x : int, y : int) -> $18 int 2literal: int
dec  = 2
hex8 = 0x02
bit8 = 0b00000010
  // Note: while the first argument is applied to `pretend-decreasing`
  // to ensure the termination, it is not decreasing. In effect, the
  // difference between `ok` and `ng` is decreasing. However at present
  // there is no way to tell it to the compiler.
  if pp: (int) -> $18 bool(mm: int) then binsearchck/binsearch/binsearch: (ok : int, ng : int, p : (int) -> $18 bool) -> $18 int(mm: int.pretend-decreasingstd/core/undiv/pretend-decreasing: (x : int) -> $18 int, ngng: int, pp: (int) -> $18 bool)
  else binsearchck/binsearch/binsearch: (ok : int, ng : int, p : (int) -> $18 bool) -> $18 int(okok: int.pretend-decreasingstd/core/undiv/pretend-decreasing: (x : int) -> $18 int, mm: int, pp: (int) -> $18 bool)

// Binary search on the interval of float64 between `ok` and `ng`.
// This function halves the interval `t` times, and returns a number close to
// the boundary of `p`, which divides a set of numbers into two intervals, all
// numbers in an interval satisfy `p`, and all numbers in another one do not.
// `p` must be monotone such that `p(ok)` = `True` and `p(ng)` = `False`.
pub fun binsearch-f64ck/binsearch/binsearch-f64: forall<e> (ok : float64, ng : float64, t : int, p : (float64) -> e bool) -> e float64(okok: float64: float64std/core/types/float64: V, ngng: float64: float64std/core/types/float64: V, tt: int: intstd/core/types/int: V, pp: (float64) -> $128 bool: float64std/core/types/float64: V -> ee: E boolstd/core/types/bool: V)result: -> 236 float64: ee: E float64std/core/types/float64: V
  if tt: int <=std/core/int/(<=): (x : int, y : int) -> $128 bool 0literal: int
dec  = 0
hex8 = 0x00
bit8 = 0b00000000 then returnreturn: float64 okok: float64
  val mm: float64 = (okok: float64 +std/num/float64/(+): (x : float64, y : float64) -> $128 float64 ngng: float64) *std/num/float64/(*): (x : float64, y : float64) -> $128 float64 0.5literal: float64
hex64= 0x1p-1
  if pp: (float64) -> $128 bool(mm: float64) then
    // Note: the third argument is (truly) decreasing.
    binsearch-f64ck/binsearch/binsearch-f64: (ok : float64, ng : float64, t : int, p : (float64) -> $128 bool) -> $128 float64(mm: float64, ngng: float64, (tt: int -std/core/int/(-): (x : int, y : int) -> $128 int 1literal: int
dec  = 1
hex8 = 0x01
bit8 = 0b00000001).pretend-decreasingstd/core/undiv/pretend-decreasing: (x : int) -> $128 int, pp: (float64) -> $128 bool)
  else
    binsearch-f64ck/binsearch/binsearch-f64: (ok : float64, ng : float64, t : int, p : (float64) -> $128 bool) -> $128 float64(okok: float64, mm: float64, (tt: int -std/core/int/(-): (x : int, y : int) -> $128 int 1literal: int
dec  = 1
hex8 = 0x01
bit8 = 0b00000001).pretend-decreasingstd/core/undiv/pretend-decreasing: (x : int) -> $128 int, pp: (float64) -> $128 bool)