/* Segment tree

Usage:

```
import ck/segtree

// 1. Define a monoid
fun mon(): monoid<int>
  Monoid(0, (+))

fun main()
  // 2. Create a segment tree
  val t = segtree(10, mon())

  // 3. Manipulate it (see below)
  t.set(1, 3)
  t.set(3, 8)
  t.product(0, 10).println // 11
```
\/
*/
module segtree

warning: Type monoid may be better declared as a value type for efficiency (e.g. 'value type/struct'),
or declared as a reference type to suppress this warning (e.g. 'ref type/struct')pub struct monoidck/segtree/monoid: V -> V<aa: V>
  oneone: 4 : aa: V
  mulmul: (4, 4) -> 4 : (aa: V, aa: V) -> astd/core/types/(<>): E

abstract struct segtreeck/segtree/segtree: (H, V) -> V<hh: H,aa: V>
  prodprod: ref<13,vector<14>> : refstd/core/types/ref: (H, V) -> V<hh: H,vectorstd/core/types/vector: V -> V<aa: V>>
  leaf-countleaf-count: int : intstd/core/types/int: V
  monmon: monoid<14> : monoidck/segtree/monoid: V -> V<aa: V>

// Create a segment tree
pub fun segtreeck/segtree/segtree: forall<a,h> (n : int, mon : monoid<a>) -> (alloc<h>) segtree<h,a>(nn: int: intstd/core/types/int: V, monmon: monoid<$1679>: monoidck/segtree/monoid: V -> V<aa: V>): allocstd/core/types/alloc: H -> X<hh: H> segtreeck/segtree/segtree: (H, V) -> V<hh: H,aa: V>
  varstd/core/hnd/local-var: forall<a,b,e,h> (init : a, action : (l : local-var<h,a>) -> <local<h>|e> b) -> <local<h>|e> b leaf-countstd/core/types/local-scope: forall<a,e> (action : forall<h> () -> <local<h>|e> a) -> e a := 1
  unsafe-no-divstd/core/types/unsafe-no-div: forall<a,e> (action : () -> <div|e> a) -> e a {
    whilestd/core/while: forall<e> (predicate : () -> <div|e> bool, action : () -> <div|e> ()) -> <div|e> () { leaf-countleaf-count: int <std/core/(<).1: (x : int, y : int) -> bool nn: int } { leaf-countleaf-count: local-var<$1684,int> :=std/core/types/local-set: forall<a,e,h> (v : local-var<h,a>, assigned : a) -> <local<h>|e> () leaf-countleaf-count: int *std/core/(*): (int, int) -> int 2 }
  }
  Segtreeck/segtree/Segtree: forall<h,a> (prod : ref<h,vector<a>>, leaf-count : int, mon : monoid<a>) -> segtree<h,a>(
    refstd/core/types/ref: forall<a,h> (value : a) -> (alloc<h>) ref<h,a>(vectorstd/core/vector.2: forall<a> (n : int, default : a) -> vector<a>(leaf-countleaf-count: int *std/core/(*): (int, int) -> int 2, monmon: monoid<$1679>.oneck/segtree/one: forall<a> (monoid : monoid<a>) -> a)),
    leaf-countleaf-count: int,
    monmon: monoid<$1679>
  )

// Get the `k`-th element.
// The first element is at position 0 (0-based).
pub fun [ck/segtree/([]): forall<a,h> (seg : segtree<h,a>, k : int) -> <read<h>,div,exn> a](^segseg: segtree<$316,$315>: segtreeck/segtree/segtree: (H, V) -> V<hh: H,aa: V>, ^kk: int: intstd/core/types/int: V): <std/core/types/(<>): Ereadstd/core/types/read: H -> X<hh: H>,divstd/core/types/div: X,exnstd/core/exn: HX> aa: V
  (!std/core/types/(!): forall<h,a,e> (ref : ref<h,a>) -> <read<h>|e> a with hdiv<h,a,e>segseg: segtree<$316,$315>.prodck/segtree/prod: forall<h,a> (segtree : segtree<h,a>) -> ref<h,vector<a>>)[std/core/([]): forall<a> (v : vector<a>, index : int) -> exn akk: int +std/core/(+).4: (x : int, y : int) -> int segseg: segtree<$316,$315>.leaf-countck/segtree/leaf-count: forall<h,a> (segtree : segtree<h,a>) -> int]

// TODO: is div removable?
inline fun recalcck/segtree/recalc: forall<a,h> (seg : segtree<h,a>, k : int) -> <read<h>,write<h>,div,exn> ()(segseg: segtree<$1378,$1377>: segtreeck/segtree/segtree: (H, V) -> V<hh: H,aa: V>, kk: int: intstd/core/types/int: V): <std/core/types/(<>): Ereadstd/core/types/read: H -> X<hh: H>,writestd/core/types/write: H -> X<hh: H>,divstd/core/types/div: X,exnstd/core/exn: HX> (std/core/types/(): V)std/core/types/(): V
  segseg: segtree<$1378,$1377>.prodck/segtree/prod: forall<h,a> (segtree : segtree<h,a>) -> ref<h,vector<a>>.modifystd/core/types/modify: forall<h,a,b,e> (ref : ref<h,a>, f : forall<h1> (local-var<h1,a>) -> <local<h1>|e> b) -> <read<h>,write<h>|e> b with hdiv<h,a,e> fn(prodprod: local-var<$1390,vector<$1377>>)
    fun looploop: (i : int) -> <pure,local<$1390>> ()(ii: int: intstd/core/types/int: V)
      if ii: int <=std/core/(<=).1: (x : int, y : int) -> bool 1 then returnreturn: () (std/core/types/(): ())std/core/types/(): ()
      val pp: int = ii: int /std/core/(/): (x : int, y : int) -> int 2
      prodprod: local-var<$1390,vector<$1377>>[std/core/([]).1: forall<a,e,h> (self : local-var<h,vector<a>>, index : int, assigned : a) -> <local<h>,exn|e> ()pp: int] := (segseg: segtree<$1378,$1377>.monck/segtree/mon: forall<h,a> (segtree : segtree<h,a>) -> monoid<a>.mulck/segtree/mul: forall<a> (monoid : monoid<a>) -> ((a, a) -> a))(prodprod: vector<$1377>[std/core/([]): forall<a> (v : vector<a>, index : int) -> exn app: int *std/core/(*): (int, int) -> int 2], prodprod: vector<$1377>[std/core/([]): forall<a> (v : vector<a>, index : int) -> exn app: int *std/core/(*): (int, int) -> int 2 +std/core/(+).4: (x : int, y : int) -> int 1])
      looploop: (i : int) -> <exn,local<$1390>,div> ()(unsafe-decreasingstd/core/types/unsafe-decreasing: forall<a> (x : a) -> a(pp: int))
    looploop: (i : int) -> <pure,local<$1390>> ()(kk: int)

// Set a value to an element.
// The first element is at position 0 (0-based).
pub fun setck/segtree/set: forall<a,h> (seg : segtree<h,a>, k : int, v : a) -> <read<h>,write<h>,div,exn> ()(segseg: segtree<$1870,$1869>: segtreeck/segtree/segtree: (H, V) -> V<hh: H,aa: V>, kk: int: intstd/core/types/int: V, vv: $1869: aa: V): <std/core/types/(<>): Ereadstd/core/types/read: H -> X<hh: H>,writestd/core/types/write: H -> X<hh: H>,divstd/core/types/div: X,exnstd/core/exn: HX> (std/core/types/(): V)std/core/types/(): V
  val k'k': int = kk: int +std/core/(+).4: (x : int, y : int) -> int segseg: segtree<$1870,$1869>.leaf-countck/segtree/leaf-count: forall<h,a> (segtree : segtree<h,a>) -> int
  segseg: segtree<$1870,$1869>.prodck/segtree/prod: forall<h,a> (segtree : segtree<h,a>) -> ref<h,vector<a>>.modifystd/core/types/modify: forall<h,a,b,e> (ref : ref<h,a>, f : forall<h1> (local-var<h1,a>) -> <local<h1>|e> b) -> <read<h>,write<h>|e> b with hdiv<h,a,e> fn(prodprod: local-var<$1896,vector<$1869>>) { prodprod: local-var<$1896,vector<$1869>>[std/core/([]).1: forall<a,e,h> (self : local-var<h,vector<a>>, index : int, assigned : a) -> <local<h>,exn|e> ()k'k': int] := vv: $1869 }
  segseg: segtree<$1870,$1869>.recalcck/segtree/recalc: forall<a,h> (seg : segtree<h,a>, k : int) -> <read<h>,write<h>,div,exn> ()(k'k': int)

// Apply a function to an element.
// The first element is at position 0 (0-based).
pub fun updateck/segtree/update: forall<a,e,h> (seg : segtree<h,a>, k : int, f : forall<h1> (a) -> <local<h1>,div,exn|e> a) -> <read<h>,write<h>,div,exn|e> ()(segseg: segtree<$1975,$1973>: segtreeck/segtree/segtree: (H, V) -> V<hh: H,aa: V>, kk: int: intstd/core/types/int: V, ff: forall<h> ($1973) -> <local<h>,div,exn|$1974> $1973: forall<h1h1: H> aa: V -> <localstd/core/types/local: H -> X<h1h1: H>,divstd/core/types/div: X,exnstd/core/exn: HX|std/core/types/(<|>): (X, E) -> Eee: E> aa: V): <readstd/core/types/read: H -> X<hh: H>,writestd/core/types/write: H -> X<hh: H>,divstd/core/types/div: X,exnstd/core/exn: HX|std/core/types/(<|>): (X, E) -> Eee: E> (std/core/types/(): V)std/core/types/(): V
  // TODO: make the type of `f` simple
  val k'k': int = kk: int +std/core/(+).4: (x : int, y : int) -> int segseg: segtree<$1975,$1973>.leaf-countck/segtree/leaf-count: forall<h,a> (segtree : segtree<h,a>) -> int
  segseg: segtree<$1975,$1973>.prodck/segtree/prod: forall<h,a> (segtree : segtree<h,a>) -> ref<h,vector<a>>.modifystd/core/types/modify: forall<h,a,b,e> (ref : ref<h,a>, f : forall<h1> (local-var<h1,a>) -> <local<h1>|e> b) -> <read<h>,write<h>|e> b with hdiv<h,a,e> fn(prodprod: local-var<$2001,vector<$1973>>)
    prodprod: local-var<$2001,vector<$1973>>[std/core/([]).1: forall<a,e,h> (self : local-var<h,vector<a>>, index : int, assigned : a) -> <local<h>,exn|e> ()k'k': int] := ff: forall<h> ($1973) -> <local<h>,div,exn|$1974> $1973(prodprod: vector<$1973>[std/core/([]): forall<a> (v : vector<a>, index : int) -> exn ak'k': int])
  segseg: segtree<$1975,$1973>.recalcck/segtree/recalc: forall<a,h> (seg : segtree<h,a>, k : int) -> <read<h>,write<h>,div,exn> ()(k'k': int)

// Return the product from the `left`-th element (inclusive) to `right`-th element (exclusive).
// The first element is at position 0 (0-based).
pub fun productck/segtree/product: forall<a,h> (seg : segtree<h,a>, left : int, right : int) -> <read<h>,div,exn> a(segseg: segtree<$833,$832>: segtreeck/segtree/segtree: (H, V) -> V<hh: H,aa: V>, leftleft: int: intstd/core/types/int: V, rightright: int: intstd/core/types/int: V): <std/core/types/(<>): Ereadstd/core/types/read: H -> X<hh: H>,divstd/core/types/div: X,exnstd/core/exn: HX> aa: V
  fun looploop: (l : int, r : int, pl : $832, pr : $832) -> <pure,read<$833>> $832(ll: int: intstd/core/types/int: V, rr: int: intstd/core/types/int: V, plpl: $832, prpr: $832)
    if ll: int <std/core/(<).1: (x : int, y : int) -> bool rr: int then
      val (std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)l'l': int, pl'pl': $832)std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b) =
        if ll: int %std/core/(%): (int, int) -> int 2 >std/core/(>).1: (x : int, y : int) -> bool 0 then
          (std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)ll: int +std/core/(+).4: (x : int, y : int) -> int 1, (segseg: segtree<$833,$832>.monck/segtree/mon: forall<h,a> (segtree : segtree<h,a>) -> monoid<a>.mulck/segtree/mul: forall<a> (monoid : monoid<a>) -> ((a, a) -> a))(plpl: $832, (!std/core/types/(!): forall<h,a,e> (ref : ref<h,a>) -> <read<h>|e> a with hdiv<h,a,e>segseg: segtree<$833,$832>.prodck/segtree/prod: forall<h,a> (segtree : segtree<h,a>) -> ref<h,vector<a>>)[std/core/([]): forall<a> (v : vector<a>, index : int) -> exn all: int]))std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)
        else
          (std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)ll: int, plpl: $832)std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)
      val (std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)r'r': int, pr'pr': $832)std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b) =
        if rr: int %std/core/(%): (int, int) -> int 2 >std/core/(>).1: (x : int, y : int) -> bool 0 then
          (std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)rr: int -std/core/(-).4: (x : int, y : int) -> int 1, (segseg: segtree<$833,$832>.monck/segtree/mon: forall<h,a> (segtree : segtree<h,a>) -> monoid<a>.mulck/segtree/mul: forall<a> (monoid : monoid<a>) -> ((a, a) -> a))((!std/core/types/(!): forall<h,a,e> (ref : ref<h,a>) -> <read<h>|e> a with hdiv<h,a,e>segseg: segtree<$833,$832>.prodck/segtree/prod: forall<h,a> (segtree : segtree<h,a>) -> ref<h,vector<a>>)[std/core/([]): forall<a> (v : vector<a>, index : int) -> exn arr: int -std/core/(-).4: (x : int, y : int) -> int 1], prpr: $832))std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)
        else
          (std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)rr: int, prpr: $832)std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)
      looploop: (l : int, r : int, pl : $832, pr : $832) -> <exn,read<$833>,div> $832(l'l': int /std/core/(/): (x : int, y : int) -> int 2, r'r': int /std/core/(/): (x : int, y : int) -> int 2, pl'pl': $832, pr'pr': $832)
    else
      (segseg: segtree<$833,$832>.monck/segtree/mon: forall<h,a> (segtree : segtree<h,a>) -> monoid<a>.mulck/segtree/mul: forall<a> (monoid : monoid<a>) -> ((a, a) -> a))(plpl: $832, prpr: $832)
  looploop: (l : int, r : int, pl : $832, pr : $832) -> <pure,read<$833>> $832(
    leftleft: int +std/core/(+).4: (x : int, y : int) -> int segseg: segtree<$833,$832>.leaf-countck/segtree/leaf-count: forall<h,a> (segtree : segtree<h,a>) -> int,
    rightright: int +std/core/(+).4: (x : int, y : int) -> int segseg: segtree<$833,$832>.leaf-countck/segtree/leaf-count: forall<h,a> (segtree : segtree<h,a>) -> int,
    segseg: segtree<$833,$832>.monck/segtree/mon: forall<h,a> (segtree : segtree<h,a>) -> monoid<a>.oneck/segtree/one: forall<a> (monoid : monoid<a>) -> a,
    segseg: segtree<$833,$832>.monck/segtree/mon: forall<h,a> (segtree : segtree<h,a>) -> monoid<a>.oneck/segtree/one: forall<a> (monoid : monoid<a>) -> a
  )

// Return the largest integer `k` such that the product from the first element
// (inclusive) to the `k`-th element (exclusive) holds `p`.
// The first element is at position 0 (0-based).
// `p` must be decreasing and the product of the empty interval must hold `p`.
pub fun binsearchck/segtree/binsearch: forall<a,e,h> (seg : segtree<h,a>, p : forall<h1> (a) -> <read<h1>,div,exn|e> bool) -> <read<h>,div,exn|e> int(segseg: segtree<$503,$501>: segtreeck/segtree/segtree: (H, V) -> V<hh: H,aa: V>, pp: forall<h> ($501) -> <read<h>,div,exn|$502> bool: forall<h1h1: H> aa: V -> <readstd/core/types/read: H -> X<h1h1: H>,divstd/core/types/div: X,exnstd/core/exn: HX|std/core/types/(<|>): (X, E) -> Eee: E> boolstd/core/types/bool: V): <readstd/core/types/read: H -> X<hh: H>,divstd/core/types/div: X,exnstd/core/exn: HX|std/core/types/(<|>): (X, E) -> Eee: E> intstd/core/types/int: V
  // TODO: make the type of `p` simple
  fun looploop: (int, int, $501, int) -> <pure,read<$503>|$502> int(kk: int, ii: int, vv: $501, ww: int)
    if ww: int ==std/core/(==).1: (x : int, y : int) -> bool 1 then returnreturn: int ii: int
    val v'v': $501 = (!std/core/types/(!): forall<h,a,e> (ref : ref<h,a>) -> <read<h>|e> a with hdiv<h,a,e>segseg: segtree<$503,$501>.prodck/segtree/prod: forall<h,a> (segtree : segtree<h,a>) -> ref<h,vector<a>>)[std/core/([]): forall<a> (v : vector<a>, index : int) -> exn akk: int *std/core/(*): (int, int) -> int 2]
    if pp: forall<h> ($501) -> <read<h>,div,exn|$502> bool((segseg: segtree<$503,$501>.monck/segtree/mon: forall<h,a> (segtree : segtree<h,a>) -> monoid<a>.mulck/segtree/mul: forall<a> (monoid : monoid<a>) -> ((a, a) -> a))(vv: $501, v'v': $501)) then
      looploop: (int, int, $501, int) -> <div,exn,read<$503>|$502> int(kk: int *std/core/(*): (int, int) -> int 2, ii: int, vv: $501, ww: int /std/core/(/): (x : int, y : int) -> int 2)
    else
      looploop: (int, int, $501, int) -> <div,exn,read<$503>|$502> int(kk: int *std/core/(*): (int, int) -> int 2 +std/core/(+).4: (x : int, y : int) -> int 1, ii: int +std/core/(+).4: (x : int, y : int) -> int ww: int /std/core/(/): (x : int, y : int) -> int 2, (segseg: segtree<$503,$501>.monck/segtree/mon: forall<h,a> (segtree : segtree<h,a>) -> monoid<a>.mulck/segtree/mul: forall<a> (monoid : monoid<a>) -> ((a, a) -> a))(vv: $501, v'v': $501), ww: int /std/core/(/): (x : int, y : int) -> int 2)
  looploop: (int, int, $501, int) -> <pure,read<$503>|$502> int(1, 0, segseg: segtree<$503,$501>.monck/segtree/mon: forall<h,a> (segtree : segtree<h,a>) -> monoid<a>.oneck/segtree/one: forall<a> (monoid : monoid<a>) -> a, segseg: segtree<$503,$501>.leaf-countck/segtree/leaf-count: forall<h,a> (segtree : segtree<h,a>) -> int)

pub fun int-add-monoidck/segtree/int-add-monoid: () -> monoid<int>(): monoidck/segtree/monoid: V -> V<intstd/core/types/int: V>
  Monoidck/segtree/Monoid: forall<a> (one : a, mul : (a, a) -> a) -> monoid<a>(0, (+)std/core/(+).4: (x : int, y : int) -> int)