// Extra functions on vectors
module vector

import random

// Quicksort
pub fun quicksortck/vector/quicksort: forall<a> (v : vector<a>, comp : (a, a) -> order) -> <pure,ndet> vector<a>(vv: vector<$378>: vectorstd/core/types/vector: V -> V<aa: V>, compcomp: ($378, $378) -> order: (aa: V, aa: V) -> orderstd/core/types/order: V): <std/core/types/(<>): Epurestd/core/pure: E,ndetstd/core/types/ndet: X> vectorstd/core/types/vector: V -> V<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 sortedstd/core/types/local-scope: forall<a,e> (action : forall<h> () -> <local<h>|e> a) -> e a := vv: vector<$378>
    fun swapswap: (i : int, j : int) -> <pure,local<$382>> ()(ii: int: intstd/core/types/int: V, jj: int: intstd/core/types/int: V)
        val tmptmp: $378 = sortedsorted: vector<$378>[std/core/([]): forall<a> (v : vector<a>, index : int) -> exn aii: int]
        sortedsorted: local-var<$382,vector<$378>>[std/core/([]).1: forall<a,e,h> (self : local-var<h,vector<a>>, index : int, assigned : a) -> <local<h>,exn|e> ()ii: int] := sortedsorted: vector<$378>[std/core/([]): forall<a> (v : vector<a>, index : int) -> exn ajj: int]
        sortedsorted: local-var<$382,vector<$378>>[std/core/([]).1: forall<a,e,h> (self : local-var<h,vector<a>>, index : int, assigned : a) -> <local<h>,exn|e> ()jj: int] := tmptmp: $378
    fun partitionpartition: forall<e> (l : int, r : int, i : int, p : ($378) -> <pure,local<$382>|e> bool) -> <pure,local<$382>|e> int(ll: int: intstd/core/types/int: V, rr: int: intstd/core/types/int: V, ii: int: intstd/core/types/int: V, pp: ($378) -> <exn,local<$382>,div|_670> bool)
        if ll: int >=std/core/(>=).1: (x : int, y : int) -> bool rr: int then
            ii: int
        elif pp: ($378) -> <exn,local<$382>,div|_670> bool(sortedsorted: vector<$378>[std/core/([]): forall<a> (v : vector<a>, index : int) -> exn all: int]) then
            swapswap: (i : int, j : int) -> <pure,local<$382>> ()(ii: int, ll: int)
            partitionpartition: (l : int, r : int, i : int, p : ($378) -> <exn,local<$382>,div|_670> bool) -> <div,exn,local<$382>|_670> int(unsafe-decreasingstd/core/types/unsafe-decreasing: forall<a> (x : a) -> a(ll: int +std/core/(+).4: (x : int, y : int) -> int 1), rr: int, ii: int +std/core/(+).4: (x : int, y : int) -> int 1, pp: ($378) -> <exn,local<$382>,div|_670> bool)
        else
            partitionpartition: (l : int, r : int, i : int, p : ($378) -> <exn,local<$382>,div|_670> bool) -> <div,exn,local<$382>|_670> int(unsafe-decreasingstd/core/types/unsafe-decreasing: forall<a> (x : a) -> a(ll: int +std/core/(+).4: (x : int, y : int) -> int 1), rr: int, ii: int, pp: ($378) -> <exn,local<$382>,div|_670> bool)
    fun sort-intlsort-intl: (l : int, r : int) -> <pure,local<$382>,ndet> ()(ll: int: intstd/core/types/int: V, rr: int: intstd/core/types/int: V)
        if rr: int -std/core/(-).4: (x : int, y : int) -> int ll: int <=std/core/(<=).1: (x : int, y : int) -> bool 1 then returnreturn: () (std/core/types/(): ())std/core/types/(): ()
        val pivot-ipivot-i: int = srandom-int32-rangestd/num/random/srandom-int32-range: (lo : int32, hi : int32) -> ndet int32(ll: int.int32std/core/int32: (i : int) -> int32, rr: int.int32std/core/int32: (i : int) -> int32).intstd/core/int.1: (i : int32) -> int
        val pivotpivot: $378 = sortedsorted: vector<$378>[std/core/([]): forall<a> (v : vector<a>, index : int) -> exn apivot-ipivot-i: int]
        swapswap: (i : int, j : int) -> <pure,local<$382>> ()(ll: int, pivot-ipivot-i: int)
        val ii: int = partitionpartition: forall<e> (l : int, r : int, i : int, p : ($378) -> <pure,local<$382>|e> bool) -> <pure,local<$382>|e> int(ll: int +std/core/(+).4: (x : int, y : int) -> int 1, rr: int, ll: int, fn(xx: $378) { compcomp: ($378, $378) -> order(xx: $378, pivotpivot: $378).is-ltstd/core/types/is-lt: (order : order) -> bool })
        val jj: int = partitionpartition: forall<e> (l : int, r : int, i : int, p : ($378) -> <pure,local<$382>|e> bool) -> <pure,local<$382>|e> int(ii: int +std/core/(+).4: (x : int, y : int) -> int 1, rr: int, ii: int, fn(xx: $378) { compcomp: ($378, $378) -> order(xx: $378, pivotpivot: $378).is-eqstd/core/types/is-eq: (order : order) -> bool })
        sort-intlsort-intl: (l : int, r : int) -> <div,exn,local<$382>,ndet> ()(ll: int, ii: int)
        sort-intlsort-intl: (l : int, r : int) -> <div,exn,local<$382>,ndet> ()(jj: int, rr: int)
    sort-intlsort-intl: (l : int, r : int) -> <pure,local<$382>,ndet> ()(0, vv: vector<$378>.lengthstd/core/length.2: forall<a> (v : vector<a>) -> int)
    sortedsorted: vector<$378>

// Return a vector whose `k`-th (0-based) element is the length of the longest
// common prefix of `v` and the suffix starting with `v[k]`.
pub fun z-algorithmck/vector/z-algorithm: forall<a> (v : vector<a>, eq : (a, a) -> bool) -> vector<int>(vv: vector<$983>: vectorstd/core/types/vector: V -> V<aa: V>, eqeq: ($983, $983) -> bool: (aa: V, aa: V) -> boolstd/core/types/bool: V): vectorstd/core/types/vector: V -> V<intstd/core/types/int: V>
  val sizesize: int = vv: vector<$983>.lengthstd/core/length.2: forall<a> (v : vector<a>) -> int
  if sizesize: int ==std/core/(==).1: (x : int, y : int) -> bool 0 then returnreturn: vector<int> vectorstd/core/vector.2: forall<a> (n : int, default : a) -> vector<a>(0, 0)std/core/types/(): ()

  unsafe-no-divstd/core/types/unsafe-no-div: forall<a,e> (action : () -> <div|e> a) -> e a {
    unsafe-no-exnstd/core/unsafe-no-exn: forall<a,e> (action : () -> <exn|e> a) -> e a {
      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 resstd/core/types/local-scope: forall<a,e> (action : forall<h> () -> <local<h>|e> a) -> e a := vectorstd/core/vector.2: forall<a> (n : int, default : a) -> vector<a>(sizesize: int, 0)
      resres: local-var<$1048,vector<int>>[std/core/([]).1: forall<a,e,h> (self : local-var<h,vector<a>>, index : int, assigned : a) -> <local<h>,exn|e> ()0] := sizesize: int

      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 ii: local-var<$1048,int> := 1
      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 jj: local-var<$1048,int> := 0
      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 kk: local-var<$1048,int> := 0
      whilestd/core/while: forall<e> (predicate : () -> <div|e> bool, action : () -> <div|e> ()) -> <div|e> () { ii: int <std/core/(<).1: (x : int, y : int) -> bool sizesize: int }
        whilestd/core/while: forall<e> (predicate : () -> <div|e> bool, action : () -> <div|e> ()) -> <div|e> () { ii: int +std/core/(+).4: (x : int, y : int) -> int jj: int <std/core/(<).1: (x : int, y : int) -> bool sizesize: int &&std/core/types/(&&): (x : bool, y : bool) -> bool eqeq: ($983, $983) -> bool(vv: vector<$983>[std/core/([]): forall<a> (v : vector<a>, index : int) -> exn ajj: int], vv: vector<$983>[std/core/([]): forall<a> (v : vector<a>, index : int) -> exn aii: int +std/core/(+).4: (x : int, y : int) -> int jj: int]) }
          jj: local-var<$1048,int> :=std/core/types/local-set: forall<a,e,h> (v : local-var<h,a>, assigned : a) -> <local<h>|e> () jj: int +std/core/(+).4: (x : int, y : int) -> int 1
        resres: local-var<$1048,vector<int>>[std/core/([]).1: forall<a,e,h> (self : local-var<h,vector<a>>, index : int, assigned : a) -> <local<h>,exn|e> ()ii: int] := jj: int
        if jj: int ==std/core/(==).1: (x : int, y : int) -> bool 0 then
          ii: local-var<$1048,int> :=std/core/types/local-set: forall<a,e,h> (v : local-var<h,a>, assigned : a) -> <local<h>|e> () ii: int +std/core/(+).4: (x : int, y : int) -> int 1
          returnreturn: () (std/core/types/(): ())std/core/types/(): ()
        kk: local-var<$1048,int> :=std/core/types/local-set: forall<a,e,h> (v : local-var<h,a>, assigned : a) -> <local<h>|e> () 1
        whilestd/core/while: forall<e> (predicate : () -> <div|e> bool, action : () -> <div|e> ()) -> <div|e> () { ii: int +std/core/(+).4: (x : int, y : int) -> int kk: int <std/core/(<).1: (x : int, y : int) -> bool sizesize: int &&std/core/types/(&&): (x : bool, y : bool) -> bool kk: int +std/core/(+).4: (x : int, y : int) -> int resres: vector<int>[std/core/([]): forall<a> (v : vector<a>, index : int) -> exn akk: int] <std/core/(<).1: (x : int, y : int) -> bool jj: int }
          resres: local-var<$1048,vector<int>>[std/core/([]).1: forall<a,e,h> (self : local-var<h,vector<a>>, index : int, assigned : a) -> <local<h>,exn|e> ()ii: int +std/core/(+).4: (x : int, y : int) -> int kk: int] := resres: vector<int>[std/core/([]): forall<a> (v : vector<a>, index : int) -> exn akk: int]
          kk: local-var<$1048,int> :=std/core/types/local-set: forall<a,e,h> (v : local-var<h,a>, assigned : a) -> <local<h>|e> () kk: int +std/core/(+).4: (x : int, y : int) -> int 1
        ii: local-var<$1048,int> :=std/core/types/local-set: forall<a,e,h> (v : local-var<h,a>, assigned : a) -> <local<h>|e> () ii: int +std/core/(+).4: (x : int, y : int) -> int kk: int
        jj: local-var<$1048,int> :=std/core/types/local-set: forall<a,e,h> (v : local-var<h,a>, assigned : a) -> <local<h>|e> () jj: int -std/core/(-).4: (x : int, y : int) -> int kk: int

      resres: vector<int>
    }
  }

// TODO: test
fun naive-searchck/vector/naive-search: forall<a> (v : vector<a>, sub : vector<a>, start : int, eq : (a, a) -> bool) -> maybe<int>(vv: vector<$61>: vectorstd/core/types/vector: V -> V<aa: V>, subsub: vector<$61>: vectorstd/core/types/vector: V -> V<aa: V>, startstart: int: intstd/core/types/int: V, eqeq: ($61, $61) -> bool: (aa: V, aa: V) -> boolstd/core/types/bool: V): maybestd/core/types/maybe: V -> V<intstd/core/types/int: V>
  fun matchingmatching: (i : int, j : int) -> bool(ii: int: intstd/core/types/int: V, jj: int: intstd/core/types/int: V): boolstd/core/types/bool: V
    if jj: int ==std/core/(==).1: (x : int, y : int) -> bool subsub: vector<$61>.lengthstd/core/length.2: forall<a> (v : vector<a>) -> int then returnreturn: bool Truestd/core/types/True: bool
    val samesame: bool = unsafe-no-exnstd/core/unsafe-no-exn: forall<a,e> (action : () -> <exn|e> a) -> e a{ eqeq: ($61, $61) -> bool(vv: vector<$61>[std/core/([]): forall<a> (v : vector<a>, index : int) -> exn aii: int +std/core/(+).4: (x : int, y : int) -> int jj: int], subsub: vector<$61>[std/core/([]): forall<a> (v : vector<a>, index : int) -> exn ajj: int]) }
    if !std/core/types/(!).1: (b : bool) -> boolsamesame: bool then returnreturn: bool Falsestd/core/types/False: bool
    matchingmatching: (i : int, j : int) -> bool(ii: int, unsafe-decreasingstd/core/types/unsafe-decreasing: forall<a> (x : a) -> a(jj: int +std/core/(+).4: (x : int, y : int) -> int 1))
  fun looploop: (i : int) -> maybe<int>(ii: int: intstd/core/types/int: V): maybestd/core/types/maybe: V -> V<intstd/core/types/int: V>
    if ii: int +std/core/(+).4: (x : int, y : int) -> int subsub: vector<$61>.lengthstd/core/length.2: forall<a> (v : vector<a>) -> int >std/core/(>).1: (x : int, y : int) -> bool vv: vector<$61>.lengthstd/core/length.2: forall<a> (v : vector<a>) -> int then returnreturn: maybe<int> Nothingstd/core/types/Nothing: forall<a> maybe<a>
    if matchingmatching: (i : int, j : int) -> bool(ii: int, 0) then returnreturn: maybe<int> Juststd/core/types/Just: forall<a> (value : a) -> maybe<a>(ii: int)std/core/types/(): ()
    looploop: (i : int) -> maybe<int>(unsafe-decreasingstd/core/types/unsafe-decreasing: forall<a> (x : a) -> a(ii: int +std/core/(+).4: (x : int, y : int) -> int 1))
  if startstart: int <std/core/(<).1: (x : int, y : int) -> bool 0 then returnreturn: maybe<int> Nothingstd/core/types/Nothing: forall<a> maybe<a>
  looploop: (i : int) -> maybe<int>(startstart: int)

// Return the position of the first occurrence of `sub` in `v`.
// The first element is at position 0 (0-based).
// `start` specifies the starting position to search.
pub fun searchck/vector/search: forall<a> (v : vector<a>, sub : vector<a>, eq : (a, a) -> bool, start : ?int) -> div maybe<int>(vv: vector<$2115>: vectorstd/core/types/vector: V -> V<aa: V>, subsub: vector<$2115>: vectorstd/core/types/vector: V -> V<aa: V>, eqeq: ($2115, $2115) -> bool: (aa: V, aa: V) -> boolstd/core/types/bool: V, startstart: ?int: intstd/core/types/optional: V -> V = 0): divstd/core/types/div: X maybestd/core/types/maybe: V -> V<intstd/core/types/int: V>
  // TODO: is div removable?
  // TODO: test
  // this optimisation works fine?
  if subsub: vector<$2115>.lengthstd/core/length.2: forall<a> (v : vector<a>) -> int <std/core/(<).1: (x : int, y : int) -> bool 16 then returnreturn: maybe<int> naive-searchck/vector/naive-search: forall<a> (v : vector<a>, sub : vector<a>, start : int, eq : (a, a) -> bool) -> maybe<int>(vv: vector<$2115>, subsub: vector<$2115>, startstart: int, eqeq: ($2115, $2115) -> bool)std/core/types/(): ()
  
  if startstart: int <std/core/(<).1: (x : int, y : int) -> bool 0 ||std/core/types/(||): (x : bool, y : bool) -> bool startstart: int +std/core/(+).4: (x : int, y : int) -> int subsub: vector<$2115>.lengthstd/core/length.2: forall<a> (v : vector<a>) -> int >std/core/(>).1: (x : int, y : int) -> bool vv: vector<$2115>.lengthstd/core/length.2: forall<a> (v : vector<a>) -> int then returnreturn: maybe<int> Nothingstd/core/types/Nothing: forall<a> maybe<a>
  // sub.length >= 16 so sub[0] exists
  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 wstd/core/types/local-scope: forall<a,e> (action : forall<h> () -> <local<h>|e> a) -> e a := vectorstd/core/vector.2: forall<a> (n : int, default : a) -> vector<a>(subsub: vector<$2115>.lengthstd/core/length.2: forall<a> (v : vector<a>) -> int +std/core/(+).4: (x : int, y : int) -> int vv: vector<$2115>.lengthstd/core/length.2: forall<a> (v : vector<a>) -> int -std/core/(-).4: (x : int, y : int) -> int startstart: int, unsafe-no-exnstd/core/unsafe-no-exn: forall<a,e> (action : () -> <exn|e> a) -> e a{ subsub: vector<$2115>[std/core/([]): forall<a> (v : vector<a>, index : int) -> exn a0] })
  forstd/core/for: forall<e> (start : int, end : int, action : (int) -> e ()) -> e () (0, subsub: vector<$2115>.lengthstd/core/length.2: forall<a> (v : vector<a>) -> int -std/core/(-).4: (x : int, y : int) -> int 1) fn(ii: int)
    unsafe-no-exnstd/core/unsafe-no-exn: forall<a,e> (action : () -> <exn|e> a) -> e a{ ww: local-var<$2123,vector<$2115>>[std/core/([]).1: forall<a,e,h> (self : local-var<h,vector<a>>, index : int, assigned : a) -> <local<h>,exn|e> ()ii: int] := subsub: vector<$2115>[std/core/([]): forall<a> (v : vector<a>, index : int) -> exn aii: int] }
  forstd/core/for: forall<e> (start : int, end : int, action : (int) -> e ()) -> e () (startstart: int, vv: vector<$2115>.lengthstd/core/length.2: forall<a> (v : vector<a>) -> int -std/core/(-).4: (x : int, y : int) -> int 1) fn(ii: int)
    unsafe-no-exnstd/core/unsafe-no-exn: forall<a,e> (action : () -> <exn|e> a) -> e a{ ww: local-var<$2123,vector<$2115>>[std/core/([]).1: forall<a,e,h> (self : local-var<h,vector<a>>, index : int, assigned : a) -> <local<h>,exn|e> ()subsub: vector<$2115>.lengthstd/core/length.2: forall<a> (v : vector<a>) -> int +std/core/(+).4: (x : int, y : int) -> int ii: int -std/core/(-).4: (x : int, y : int) -> int startstart: int] := vv: vector<$2115>[std/core/([]): forall<a> (v : vector<a>, index : int) -> exn aii: int] }
  val ll: vector<int> = z-algorithmck/vector/z-algorithm: forall<a> (v : vector<a>, eq : (a, a) -> bool) -> vector<int>(ww: vector<$2115>, eqeq: ($2115, $2115) -> bool)
  fun looploop: (i : int) -> maybe<int>(ii: int: intstd/core/types/int: V): maybestd/core/types/maybe: V -> V<intstd/core/types/int: V>
    if ii: int +std/core/(+).4: (x : int, y : int) -> int subsub: vector<$2115>.lengthstd/core/length.2: forall<a> (v : vector<a>) -> int >std/core/(>).1: (x : int, y : int) -> bool vv: vector<$2115>.lengthstd/core/length.2: forall<a> (v : vector<a>) -> int then returnreturn: maybe<int> Nothingstd/core/types/Nothing: forall<a> maybe<a>
    val foundfound: bool = unsafe-no-exnstd/core/unsafe-no-exn: forall<a,e> (action : () -> <exn|e> a) -> e a{ ll: vector<int>[std/core/([]): forall<a> (v : vector<a>, index : int) -> exn asubsub: vector<$2115>.lengthstd/core/length.2: forall<a> (v : vector<a>) -> int +std/core/(+).4: (x : int, y : int) -> int ii: int -std/core/(-).4: (x : int, y : int) -> int startstart: int] >=std/core/(>=).1: (x : int, y : int) -> bool subsub: vector<$2115>.lengthstd/core/length.2: forall<a> (v : vector<a>) -> int }
    if foundfound: bool then returnreturn: maybe<int> Juststd/core/types/Just: forall<a> (value : a) -> maybe<a>(ii: int)std/core/types/(): ()
    looploop: (i : int) -> maybe<int>(unsafe-decreasingstd/core/types/unsafe-decreasing: forall<a> (x : a) -> a(ii: int +std/core/(+).4: (x : int, y : int) -> int 1))
  looploop: (i : int) -> maybe<int>(startstart: int)