/*---------------------------------------------------------------------------
  Copyright 2012-2024, Microsoft Research, Daan Leijen.

  This is free software; you can redistribute it and/or modify it under the
  terms of the Apache License, Version 2.0. A copy of the License can be
  found in the LICENSE file at the root of this distribution.
---------------------------------------------------------------------------*/

// Standard vector functions.
module std/core/vectorstd/core/vector

import std/core/typesstd/core/types
import std/core/undivstd/core/undiv
import std/core/hndstd/core/hnd
import std/core/exnstd/core/exn
import std/core/intstd/core/int

extern import
  c  file "inline/vector"
  js file "inline/vector.js"

// ----------------------------------------------------------------------------
//  Vectors
// ----------------------------------------------------------------------------

// Return the element at position `index`  in vector `v`  without bounds check!
inline extern unsafe-idxstd/core/vector/unsafe-idx: forall<a> (v : vector<a>, index : ssize_t) -> a( ^v : vectorstd/core/types/vector: V -> V<aa: V>, index : ssize_tstd/core/types/ssize_t: V ) : totalstd/core/types/total: E aa: V
  c  "kk_vector_at_borrow"
  cs inline "(#1)[#2]"
  js inline "(#1)[#2]"

inline extern unsafe-assignstd/core/vector/unsafe-assign: forall<a> (v : vector<a>, i : ssize_t, x : a) -> () : forall<aa: V> ( v : vectorstd/core/types/vector: V -> V<aa: V>, i : ssize_tstd/core/types/ssize_t: V, x : aa: V ) -> totalstd/core/types/total: E (std/core/types/unit: V)std/core/types/unit: V
  c "kk_vector_unsafe_assign"
  cs inline "(#1)[#2] = #3"
  js inline "(#1)[#2] = #3"

inline extern unsafe-vectorstd/core/vector/unsafe-vector: forall<a> (n : ssize_t) -> vector<a> : forall<aa: V> ( n : ssize_tstd/core/types/ssize_t: V ) -> totalstd/core/types/total: E vectorstd/core/types/vector: V -> V<aa: V>
  c  inline "kk_vector_alloc(#1,kk_box_null(),kk_context())"
  cs inline "(new ##1[#1])"
  js inline "Array(#1)"

pub extern @unsafe-vector : forall<aa: V> ( n : ssize_tstd/core/types/ssize_t: V ) -> totalstd/core/types/total: E vectorstd/core/types/vector: V -> V<aa: V>
  c  inline "kk_vector_alloc(#1,kk_box_null(),kk_context())"
  cs inline "(new ##1[#1])"
  js inline "Array(#1)"

// Assign to an entry in a local `:vector` variable.
pub inline extern @index( ^self : local-varstd/core/types/local-var: (H, V) -> V<ss: H,vectorstd/core/types/vector: V -> V<aa: V>>, ^index : intstd/core/types/int: V, assigned : aa: V ) : <localstd/core/types/local: H -> X<ss: H>,exnstd/core/exn/exn: (E, V) -> V|std/core/types/effect-extend: (X, E) -> Eee: E> (std/core/types/unit: V)std/core/types/unit: V
  c  "kk_ref_vector_assign_borrow"
  cs inline "(#1)[(int)#2] = #3"  // check bounds?
  js inline "(#1)[#2] = #3"       // todo: check bounds!

// Length of a vector.
inline extern lengthzstd/core/vector/lengthz: forall<a> (v : vector<a>) -> ssize_t( ^v : vectorstd/core/types/vector: V -> V<aa: V> ) : ssize_tstd/core/types/ssize_t: V
  c  "kk_vector_len_borrow"
  cs inline "((#1).Length)"
  js inline "((#1).length)"

// Create a new vector of length `n`  with initial elements `init`` .
extern vector-allocstd/core/vector/vector-alloc: forall<a,e> (n : ssize_t, init : a) -> e vector<a>(nn: ssize_t : ssize_tstd/core/types/ssize_t: V, initinit: $231 : aa: V) : ee: E vectorstd/core/types/vector: V -> V<aa: V>
  c "kk_vector_alloc"
  cs inline "Primitive.NewArray<##1>(#1,#2)"
  js inline "_vector_initz(#1,#2)"

// Create a new vector of length `n`  with initial elements given by a total function `f` .
extern vector-alloc-totalstd/core/vector/vector-alloc-total: forall<a> (n : ssize_t, f : (ssize_t) -> a) -> vector<a>(nn: ssize_t : ssize_tstd/core/types/ssize_t: V, ff: (ssize_t) -> $259 : ssize_tstd/core/types/ssize_t: V -> astd/core/types/total: E) : vectorstd/core/types/vector: V -> V<aa: V>
  c "kk_vector_init_total"
  cs inline "Primitive.NewArray<##1>(#1,#2)"
  js inline "_vector_initf(#1,#2)"

// Create an empty vector.
pub inline extern unit/vectorstd/core/vector/unit/vector: forall<a> () -> vector<a> : forall<aa: V> () -> vectorstd/core/types/vector: V -> V<aa: V>
  c inline "kk_vector_empty()"
  cs inline "new ##1[0]"
  js inline "[]"


// Return the element at position `index`  in vector `v`.
// Raise an out of bounds exception if `index < 0`  or `index >= v.length`.
pub fun @index( ^vv: vector<$281> : vectorstd/core/types/vector: V -> V<aa: V>, ^indexindex: int : intstd/core/types/int: V )result: -> exn 329 : exnstd/core/exn/exn: (E, V) -> V aa: V
  val idxidx: ssize_t = indexindex: int.ssize_tstd/core/int/ssize_t: (i : int) -> exn ssize_t()
  if idxidx: ssize_t <std/core/vector/ssize_t/(<): (ssize_t, ssize_t) -> exn bool vv: vector<$281>.lengthzstd/core/vector/lengthz: (v : vector<$281>) -> exn ssize_t then unsafe-idxstd/core/vector/unsafe-idx: (v : vector<$281>, index : ssize_t) -> exn $281(vv: vector<$281>,idxidx: ssize_t) else throwstd/core/exn/throw: (message : string, info : ? exception-info) -> exn $281("index out of bounds"literal: string
count= 19,ExnRangestd/core/exn/ExnRange: exception-info)

// Return the element at position `index` in vector `v`, or `Nothing` if out of bounds
pub fun atstd/core/vector/at: forall<a> (v : vector<a>, index : int) -> maybe<a>( ^vv: vector<$334> : vectorstd/core/types/vector: V -> V<aa: V>, ^indexindex: int : intstd/core/types/int: V )result: -> total maybe<377> : maybestd/core/types/maybe: V -> V<aa: V>
  val idxidx: ssize_t = indexindex: int.ssize_tstd/core/int/ssize_t: (i : int) -> ssize_t
  if idxidx: ssize_t <std/core/vector/ssize_t/(<): (ssize_t, ssize_t) -> bool vv: vector<$334>.lengthzstd/core/vector/lengthz: (v : vector<$334>) -> ssize_t then Juststd/core/types/Just: forall<a> (value : a) -> maybe<a>(unsafe-idxstd/core/vector/unsafe-idx: (v : vector<$334>, index : ssize_t) -> $334(vv: vector<$334>,idxidx: ssize_t)) else Nothingstd/core/types/Nothing: forall<a> maybe<a>

// Return the length of a vector.
pub fun lengthstd/core/vector/length: forall<a> (v : vector<a>) -> int( ^vv: vector<$382> : vectorstd/core/types/vector: V -> V<aa: V> )result: -> total int : intstd/core/types/int: V
  vv: vector<$382>.lengthzstd/core/vector/lengthz: (v : vector<$382>) -> ssize_t.intstd/core/int/ssize_t/int: (i : ssize_t) -> int

// Create a new vector of length `n`  with initial elements `default` .
pub fun vectorstd/core/vector/vector: forall<a> (n : int, default : a) -> vector<a>( ^nn: int : intstd/core/types/int: V, defaultdefault: $404 : aa: V)result: -> total vector<423> : vectorstd/core/types/vector: V -> V<aa: V>
  vector-allocstd/core/vector/vector-alloc: (n : ssize_t, init : $404) -> vector<$404>(nn: int.ssize_tstd/core/int/ssize_t: (i : int) -> ssize_t, defaultdefault: $404)

// Create a new vector of length `n`  with initial elements given by _total_ function `f`.
// (can be more efficient than `vector-init`)
pub fun vector-init-totalstd/core/vector/vector-init-total: forall<a> (n : int, f : (int) -> a) -> vector<a>( ^nn: int : intstd/core/types/int: V, ff: (int) -> $428 : intstd/core/types/int: V -> astd/core/types/total: E )result: -> total vector<454> : vectorstd/core/types/vector: V -> V<aa: V>
  vector-alloc-totalstd/core/vector/vector-alloc-total: (n : ssize_t, f : (ssize_t) -> $428) -> vector<$428>( nn: int.ssize_tstd/core/int/ssize_t: (i : int) -> ssize_t, fnfn: (i : ssize_t) -> $428(ii: ssize_t) ff: (int) -> $428(ii: ssize_t.intstd/core/int/ssize_t/int: (i : ssize_t) -> int) )

// Create a new vector of length `n`  with initial elements given by function `f` which can have a control effect.
pub fun vector-initstd/core/vector/vector-init: forall<a,e> (n : int, f : (int) -> e a) -> e vector<a>( ^nn: int : intstd/core/types/int: V, ff: (int) -> $506 $505 : intstd/core/types/int: V -> ee: E aa: V )result: -> 548 vector<547> : ee: E vectorstd/core/types/vector: V -> V<aa: V>
  val lenlen: ssize_t = nn: int.ssize_tstd/core/int/ssize_t: (i : int) -> $506 ssize_t
  val vv: vector<$505> = unsafe-vectorstd/core/vector/unsafe-vector: (n : ssize_t) -> $506 vector<$505>(lenlen: ssize_t)
  forzstd/core/vector/forz: (n : ssize_t, action : (ssize_t) -> $506 ()) -> $506 ()( lenlen: ssize_t ) fnfn: (i : ssize_t) -> $506 ()(ii: ssize_t)
    unsafe-assignstd/core/vector/unsafe-assign: (v : vector<$505>, i : ssize_t, x : $505) -> $506 ()(vv: vector<$505>,ii: ssize_t,ff: (int) -> $506 $505(ii: ssize_t.intstd/core/int/ssize_t/int: (i : ssize_t) -> $506 int))
  vv: vector<$505>

// Invoke a function `f` for each element in a vector `v`
pub fun foreachstd/core/vector/foreach: forall<a,e> (v : vector<a>, f : (a) -> e ()) -> e ()( vv: vector<$596> : vectorstd/core/types/vector: V -> V<aa: V>, ff: ($596) -> $597 () : (aa: V) -> ee: E (std/core/types/unit: V)std/core/types/unit: V )result: -> 619 () : ee: E (std/core/types/unit: V)std/core/types/unit: V
  vv: vector<$596>.foreach-indexedzstd/core/vector/foreach-indexedz: (v : vector<$596>, f : (ssize_t, $596) -> $597 ()) -> $597 ()( fnfn: (ssize_t, x : $596) -> $597 ()(_,xx: $596) { ff: ($596) -> $597 ()(xx: $596) })

// Invoke a function `f` for each element in a vector `v`
pub fun foreach-indexedstd/core/vector/foreach-indexed: forall<a,e> (v : vector<a>, f : (int, a) -> e ()) -> e ()( vv: vector<$626> : vectorstd/core/types/vector: V -> V<aa: V>, ff: (int, $626) -> $627 () : (intstd/core/types/int: V,aa: V) -> ee: E (std/core/types/unit: V)std/core/types/unit: V )result: -> 653 () : ee: E (std/core/types/unit: V)std/core/types/unit: V
  foreach-indexedzstd/core/vector/foreach-indexedz: (v : vector<$626>, f : (ssize_t, $626) -> $627 ()) -> $627 ()( vv: vector<$626>, fnfn: (i : ssize_t, x : $626) -> $627 ()(ii: ssize_t,xx: $626) { ff: (int, $626) -> $627 ()(ii: ssize_t.intstd/core/int/ssize_t/int: (i : ssize_t) -> $627 int,xx: $626) } )

fun foreach-indexedzstd/core/vector/foreach-indexedz: forall<a,e> (v : vector<a>, f : (ssize_t, a) -> e ()) -> e ()( vv: vector<$555> : vectorstd/core/types/vector: V -> V<aa: V>, ff: (ssize_t, $555) -> $556 () : (ssize_tstd/core/types/ssize_t: V,aa: V) -> ee: E (std/core/types/unit: V)std/core/types/unit: V )result: -> 589 () : ee: E (std/core/types/unit: V)std/core/types/unit: V
  forzstd/core/vector/forz: (n : ssize_t, action : (ssize_t) -> $556 ()) -> $556 ()( vv: vector<$555>.lengthzstd/core/vector/lengthz: (v : vector<$555>) -> $556 ssize_t ) fnfn: (i : ssize_t) -> $556 ()(ii: ssize_t)
    ff: (ssize_t, $555) -> $556 ()(ii: ssize_t,vv: vector<$555>.unsafe-idxstd/core/vector/unsafe-idx: (v : vector<$555>, index : ssize_t) -> $556 $555(ii: ssize_t))

// Invoke a function `f` for each element in a vector `v`.
// If `f` returns `Just`, the iteration is stopped early and the result is returned.
pub fun foreach-whilestd/core/vector/foreach-while: forall<a,b,e> (v : vector<a>, f : (a) -> e maybe<b>) -> e maybe<b>( vv: vector<$724> : vectorstd/core/types/vector: V -> V<aa: V>, ff: ($724) -> $726 maybe<$725> : aa: V -> ee: E maybestd/core/types/maybe: V -> V<bb: V> )result: -> 766 maybe<765> : ee: E maybestd/core/types/maybe: V -> V<bb: V>
  for-whilezstd/core/vector/for-whilez: (n : ssize_t, action : (ssize_t) -> $726 maybe<$725>) -> $726 maybe<$725>( vv: vector<$724>.lengthzstd/core/vector/lengthz: (v : vector<$724>) -> $726 ssize_t ) fnfn: (i : ssize_t) -> $726 maybe<$725>(ii: ssize_t)
    ff: ($724) -> $726 maybe<$725>(vv: vector<$724>.unsafe-idxstd/core/vector/unsafe-idx: (v : vector<$724>, index : ssize_t) -> $726 $724(ii: ssize_t))

// Apply a function `f` to each element in a vector `v`
pub fun mapstd/core/vector/map: forall<a,b,e> (v : vector<a>, f : (a) -> e b) -> e vector<b>( vv: vector<$776> : vectorstd/core/types/vector: V -> V<aa: V>, ff: ($776) -> $778 $777 : aa: V -> ee: E bb: V )result: -> 830 vector<829> : ee: E vectorstd/core/types/vector: V -> V<bb: V>
  val ww: vector<$777> = unsafe-vectorstd/core/vector/unsafe-vector: (n : ssize_t) -> $778 vector<$777>(vv: vector<$776>.lengthstd/core/vector/length: (v : vector<$776>) -> $778 int.ssize_tstd/core/int/ssize_t: (i : int) -> $778 ssize_t)
  vv: vector<$776>.foreach-indexedzstd/core/vector/foreach-indexedz: (v : vector<$776>, f : (ssize_t, $776) -> $778 ()) -> $778 () fnfn: (i : ssize_t, x : $776) -> $778 ()(ii: ssize_t,xx: $776)
    unsafe-assignstd/core/vector/unsafe-assign: (v : vector<$777>, i : ssize_t, x : $777) -> $778 ()(ww: vector<$777>,ii: ssize_t,ff: ($776) -> $778 $777(xx: $776))
  ww: vector<$777>

// Convert a vector to a list.
pub fun liststd/core/vector/list: forall<a> (v : vector<a>) -> list<a>( vv: vector<$866> : vectorstd/core/types/vector: V -> V<aa: V> )result: -> total list<883> : liststd/core/types/list: V -> V<aa: V>
  vv: vector<$866>.vliststd/core/vector/vlist: (v : vector<$866>, tail : ? (list<$866>)) -> list<$866>

// Convert a vector to a list with an optional tail.
pub extern vliststd/core/vector/vlist: forall<a> (v : vector<a>, tail : ? (list<a>)) -> list<a>( vv: vector<$840> : vectorstd/core/types/vector: V -> V<aa: V>, tailtail: ? (list<$840>) : liststd/core/types/list: V -> V<aa: V> = [std/core/types/Nil: forall<a> list<a>]std/core/types/Nil: forall<a> list<a> ) : liststd/core/types/list: V -> V<aa: V>
  c  "kk_vector_to_list"
  cs inline "Primitive.VList<##1>(#1,#2)"
  js inline "_vlist(#1,#2)"

// Convert a list to a vector.
pub fun list/vectorstd/core/vector/list/vector: forall<a> (xs : list<a>) -> vector<a>( xsxs: list<$907> : liststd/core/types/list: V -> V<aa: V> )result: -> total vector<921> : vectorstd/core/types/vector: V -> V<aa: V>
  xsxs: list<$907>.unvliststd/core/vector/unvlist: (xs : list<$907>) -> vector<$907>

extern unvliststd/core/vector/unvlist: forall<a> (xs : list<a>) -> vector<a>( xsxs: list<$888> : liststd/core/types/list: V -> V<aa: V> ) : vectorstd/core/types/vector: V -> V<aa: V>
  c  "kk_list_to_vector"
  cs inline "Primitive.UnVList<##1>(#1)"
  js inline "_unvlist(#1)"


// Executes `action` `n` times for each integer between [`0`,`n`)  (excluding `n` ).
// If `n <= 0`  the function returns without any call to `action` .
fun forzstd/core/vector/forz: forall<e> (n : ssize_t, action : (ssize_t) -> e ()) -> e ()( nn: ssize_t : ssize_tstd/core/types/ssize_t: V, actionaction: (ssize_t) -> $466 () : (ssize_tstd/core/types/ssize_t: V) -> ee: E (std/core/types/unit: V)std/core/types/unit: V )result: -> 501 () : ee: E (std/core/types/unit: V)std/core/types/unit: V
  fun reprep: (i : ssize_t) -> $466 ()( ii: ssize_t : ssize_tstd/core/types/ssize_t: V )result: -> $466 ()
    if ii: ssize_t <std/core/vector/ssize_t/(<): (ssize_t, ssize_t) -> $466 bool nn: ssize_t then
      actionaction: (ssize_t) -> $466 ()(ii: ssize_t)
      reprep: (i : ssize_t) -> $466 ()(pretend-decreasingstd/core/undiv/pretend-decreasing: (x : ssize_t) -> $466 ssize_t(ii: ssize_t.incrstd/core/vector/ssize_t/incr: (i : ssize_t) -> $466 ssize_t))std/core/types/Unit: ()
  reprep: (i : ssize_t) -> $466 ()(0literal: int
dec  = 0
hex8 = 0x00
bit8 = 0b00000000.ssize_tstd/core/int/ssize_t: (i : int) -> $466 ssize_t)

// Executes `action` at most `n` times for each integer between `0`  upto `n`  (excluding `n` ).
// If `n <= 0`  the function returns without any call to `action` .
// If `action` returns `Just`, the iteration is stopped and the result returned
fun for-whilezstd/core/vector/for-whilez: forall<a,e> (n : ssize_t, action : (ssize_t) -> e maybe<a>) -> e maybe<a>( nn: ssize_t : ssize_tstd/core/types/ssize_t: V, actionaction: (ssize_t) -> $661 maybe<$660> : (ssize_tstd/core/types/ssize_t: V) -> ee: E maybestd/core/types/maybe: V -> V<aa: V> )result: -> 717 maybe<716> : ee: E maybestd/core/types/maybe: V -> V<aa: V>
  fun reprep: (i : ssize_t) -> $661 maybe<$660>( ii: ssize_t : ssize_tstd/core/types/ssize_t: V )result: -> $661 maybe<$660>
    if ii: ssize_t <std/core/vector/ssize_t/(<): (ssize_t, ssize_t) -> $661 bool nn: ssize_t then
      match actionaction: (ssize_t) -> $661 maybe<$660>(ii: ssize_t)
        Nothingstd/core/types/Nothing: forall<a> maybe<a> -> reprep: (i : ssize_t) -> $661 maybe<$660>(pretend-decreasingstd/core/undiv/pretend-decreasing: (x : ssize_t) -> $661 ssize_t(ii: ssize_t.incrstd/core/vector/ssize_t/incr: (i : ssize_t) -> $661 ssize_t))
        Juststd/core/types/Just: forall<a> (value : a) -> maybe<a>(xx: $660) -> Juststd/core/types/Just: forall<a> (value : a) -> maybe<a>(xx: $660)
    else Nothingstd/core/types/Nothing: forall<a> maybe<a>
  reprep: (i : ssize_t) -> $661 maybe<$660>(0literal: int
dec  = 0
hex8 = 0x00
bit8 = 0b00000000.ssize_tstd/core/int/ssize_t: (i : int) -> $661 ssize_t)




// Minimal set of operations that we need in `std/core`.
inline fip extern ssize_t/(<=)std/core/vector/ssize_t/(<=): (ssize_t, ssize_t) -> bool : (ssize_tstd/core/types/ssize_t: V,ssize_tstd/core/types/ssize_t: V) -> boolstd/core/types/bool: V
  inline "(#1 <= #2)"

inline fip extern ssize_t/(>=)std/core/vector/ssize_t/(>=): (ssize_t, ssize_t) -> bool : (ssize_tstd/core/types/ssize_t: V,ssize_tstd/core/types/ssize_t: V) -> boolstd/core/types/bool: V
  inline "(#1 >= #2)"

inline fip extern ssize_t/(<)std/core/vector/ssize_t/(<): (ssize_t, ssize_t) -> bool  : (ssize_tstd/core/types/ssize_t: V,ssize_tstd/core/types/ssize_t: V) -> boolstd/core/types/bool: V
  inline "(#1 < #2)"

inline fip extern ssize_t/(+)std/core/vector/ssize_t/(+): (ssize_t, ssize_t) -> ssize_t  : (ssize_tstd/core/types/ssize_t: V,ssize_tstd/core/types/ssize_t: V) -> ssize_tstd/core/types/ssize_t: V
  inline "(#1 + #2)"
  js inline "((#1 + #2)|0)"

inline fip extern ssize_t/(-)std/core/vector/ssize_t/(-): (ssize_t, ssize_t) -> ssize_t  : (ssize_tstd/core/types/ssize_t: V,ssize_tstd/core/types/ssize_t: V) -> ssize_tstd/core/types/ssize_t: V
  inline "(#1 - #2)"
  js inline "((#1 - #2)|0)"

inline fip extern ssize_t/is-posstd/core/vector/ssize_t/is-pos: (i : ssize_t) -> bool( i : ssize_tstd/core/types/ssize_t: V ) : boolstd/core/types/bool: V
  inline "(#1 > 0)"

inline fip extern ssize_t/is-negstd/core/vector/ssize_t/is-neg: (i : ssize_t) -> bool( i : ssize_tstd/core/types/ssize_t: V ) : boolstd/core/types/bool: V
  inline "(#1 < 0)"

fip extern ssize_t/is-zerostd/core/vector/ssize_t/is-zero: (i : ssize_t) -> bool( ii: ssize_t : ssize_tstd/core/types/ssize_t: V ) : boolstd/core/types/bool: V
  inline "(#1 == 0)"
  js inline "(#1 === 0)"

fip extern ssize_t/decrstd/core/vector/ssize_t/decr: (i : ssize_t) -> ssize_t(ii: ssize_t : ssize_tstd/core/types/ssize_t: V ) : ssize_tstd/core/types/ssize_t: V
  inline "(#1 - 1)"

fip extern ssize_t/incrstd/core/vector/ssize_t/incr: (i : ssize_t) -> ssize_t(ii: ssize_t : ssize_tstd/core/types/ssize_t: V ) : ssize_tstd/core/types/ssize_t: V
  inline "(#1 + 1)"