/*---------------------------------------------------------------------------
  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)"

// 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: $375 : 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) -> $399 : 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<$206> : vectorstd/core/types/vector: V -> V<aa: V>, ^indexindex: int : intstd/core/types/int: V )result: -> exn 252 : 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<$206>.lengthzstd/core/vector/lengthz: (v : vector<$206>) -> exn ssize_t then unsafe-idxstd/core/vector/unsafe-idx: (v : vector<$206>, index : ssize_t) -> exn $206(vv: vector<$206>,idxidx: ssize_t) else throwstd/core/exn/throw: (message : string, info : ? exception-info) -> exn $206("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<$261> : vectorstd/core/types/vector: V -> V<aa: V>, ^indexindex: int : intstd/core/types/int: V )result: -> total maybe<302> : 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<$261>.lengthzstd/core/vector/lengthz: (v : vector<$261>) -> ssize_t then Juststd/core/types/Just: forall<a> (value : a) -> maybe<a>(unsafe-idxstd/core/vector/unsafe-idx: (v : vector<$261>, index : ssize_t) -> $261(vv: vector<$261>,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<$314> : vectorstd/core/types/vector: V -> V<aa: V> )result: -> total int : intstd/core/types/int: V
  vv: vector<$314>.lengthzstd/core/vector/lengthz: (v : vector<$314>) -> 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: $746 : aa: V)result: -> total vector<763> : vectorstd/core/types/vector: V -> V<aa: V>
  vector-allocstd/core/vector/vector-alloc: (n : ssize_t, init : $746) -> vector<$746>(nn: int.ssize_tstd/core/int/ssize_t: (i : int) -> ssize_t, defaultdefault: $746)

// 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,e> (n : int, f : (int) -> a) -> e vector<a>( ^nn: int : intstd/core/types/int: V, ff: (int) -> $817 : intstd/core/types/int: V -> astd/core/types/total: E )result: -> 844 vector<843> : ee: E vectorstd/core/types/vector: V -> V<aa: V>
  vector-alloc-totalstd/core/vector/vector-alloc-total: (n : ssize_t, f : (ssize_t) -> $817) -> $818 vector<$817>( nn: int.ssize_tstd/core/int/ssize_t: (i : int) -> $818 ssize_t, fnfn: (i : ssize_t) -> $817(ii: ssize_t) ff: (int) -> $817(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) -> $772 $771 : intstd/core/types/int: V -> ee: E aa: V )result: -> 810 vector<809> : ee: E vectorstd/core/types/vector: V -> V<aa: V>
  val lenlen: ssize_t = nn: int.ssize_tstd/core/int/ssize_t: (i : int) -> $772 ssize_t
  val vv: vector<$771> = unsafe-vectorstd/core/vector/unsafe-vector: (n : ssize_t) -> $772 vector<$771>(lenlen: ssize_t)
  forzstd/core/vector/forz: (n : ssize_t, action : (ssize_t) -> $772 ()) -> $772 ()( lenlen: ssize_t ) fnfn: (i : ssize_t) -> $772 ()(ii: ssize_t)
    unsafe-assignstd/core/vector/unsafe-assign: (v : vector<$771>, i : ssize_t, x : $771) -> $772 ()(vv: vector<$771>,ii: ssize_t,ff: (int) -> $772 $771(ii: ssize_t.intstd/core/int/ssize_t/int: (i : ssize_t) -> $772 int))
  vv: vector<$771>

// 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<$566> : vectorstd/core/types/vector: V -> V<aa: V>, ff: ($566) -> $567 () : (aa: V) -> ee: E (std/core/types/unit: V)std/core/types/unit: V )result: -> 585 () : ee: E (std/core/types/unit: V)std/core/types/unit: V
  vv: vector<$566>.foreach-indexedzstd/core/vector/foreach-indexedz: (v : vector<$566>, f : (ssize_t, $566) -> $567 ()) -> $567 ()( fnfn: (ssize_t, x : $566) -> $567 ()(_,xx: $566) { ff: ($566) -> $567 ()(xx: $566) })

// 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<$592> : vectorstd/core/types/vector: V -> V<aa: V>, ff: (int, $592) -> $593 () : (intstd/core/types/int: V,aa: V) -> ee: E (std/core/types/unit: V)std/core/types/unit: V )result: -> 615 () : ee: E (std/core/types/unit: V)std/core/types/unit: V
  foreach-indexedzstd/core/vector/foreach-indexedz: (v : vector<$592>, f : (ssize_t, $592) -> $593 ()) -> $593 ()( vv: vector<$592>, fnfn: (i : ssize_t, x : $592) -> $593 ()(ii: ssize_t,xx: $592) { ff: (int, $592) -> $593 ()(ii: ssize_t.intstd/core/int/ssize_t/int: (i : ssize_t) -> $593 int,xx: $592) } )

fun foreach-indexedzstd/core/vector/foreach-indexedz: forall<a,e> (v : vector<a>, f : (ssize_t, a) -> e ()) -> e ()( vv: vector<$529> : vectorstd/core/types/vector: V -> V<aa: V>, ff: (ssize_t, $529) -> $530 () : (ssize_tstd/core/types/ssize_t: V,aa: V) -> ee: E (std/core/types/unit: V)std/core/types/unit: V )result: -> 559 () : ee: E (std/core/types/unit: V)std/core/types/unit: V
  forzstd/core/vector/forz: (n : ssize_t, action : (ssize_t) -> $530 ()) -> $530 ()( vv: vector<$529>.lengthzstd/core/vector/lengthz: (v : vector<$529>) -> $530 ssize_t ) fnfn: (i : ssize_t) -> $530 ()(ii: ssize_t)
    ff: (ssize_t, $529) -> $530 ()(ii: ssize_t,vv: vector<$529>.unsafe-idxstd/core/vector/unsafe-idx: (v : vector<$529>, index : ssize_t) -> $530 $529(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<$622> : vectorstd/core/types/vector: V -> V<aa: V>, ff: ($622) -> $624 maybe<$623> : aa: V -> ee: E maybestd/core/types/maybe: V -> V<bb: V> )result: -> 658 maybe<657> : ee: E maybestd/core/types/maybe: V -> V<bb: V>
  for-whilezstd/core/vector/for-whilez: (n : ssize_t, action : (ssize_t) -> $624 maybe<$623>) -> $624 maybe<$623>( vv: vector<$622>.lengthzstd/core/vector/lengthz: (v : vector<$622>) -> $624 ssize_t ) fnfn: (i : ssize_t) -> $624 maybe<$623>(ii: ssize_t)
    ff: ($622) -> $624 maybe<$623>(vv: vector<$622>.unsafe-idxstd/core/vector/unsafe-idx: (v : vector<$622>, index : ssize_t) -> $624 $622(ii: ssize_t))

// Apply a total 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<$688> : vectorstd/core/types/vector: V -> V<aa: V>, ff: ($688) -> $690 $689 : aa: V -> ee: E bb: V )result: -> 736 vector<735> : ee: E vectorstd/core/types/vector: V -> V<bb: V>
  val ww: vector<$689> = unsafe-vectorstd/core/vector/unsafe-vector: (n : ssize_t) -> $690 vector<$689>(vv: vector<$688>.lengthstd/core/vector/length: (v : vector<$688>) -> $690 int.ssize_tstd/core/int/ssize_t: (i : int) -> $690 ssize_t)
  vv: vector<$688>.foreach-indexedzstd/core/vector/foreach-indexedz: (v : vector<$688>, f : (ssize_t, $688) -> $690 ()) -> $690 () fnfn: (i : ssize_t, x : $688) -> $690 ()(ii: ssize_t,xx: $688)
    unsafe-assignstd/core/vector/unsafe-assign: (v : vector<$689>, i : ssize_t, x : $689) -> $690 ()(ww: vector<$689>,ii: ssize_t,ff: ($688) -> $690 $689(xx: $688))
  ww: vector<$689>

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

// 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<$334> : vectorstd/core/types/vector: V -> V<aa: V>, tailtail: ? (list<$334>) : 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<$851> : liststd/core/types/list: V -> V<aa: V> )result: -> total vector<863> : vectorstd/core/types/vector: V -> V<aa: V>
  xsxs: list<$851>.unvliststd/core/vector/unvlist: (xs : list<$851>) -> vector<$851>

extern unvliststd/core/vector/unvlist: forall<a> (xs : list<a>) -> vector<a>( xsxs: list<$358> : 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) -> $492 () : (ssize_tstd/core/types/ssize_t: V) -> ee: E (std/core/types/unit: V)std/core/types/unit: V )result: -> 525 () : ee: E (std/core/types/unit: V)std/core/types/unit: V
  fun reprep: (i : ssize_t) -> $492 ()( ii: ssize_t : ssize_tstd/core/types/ssize_t: V )result: -> $492 ()
    if ii: ssize_t <std/core/vector/ssize_t/(<): (ssize_t, ssize_t) -> $492 bool nn: ssize_t then
      actionaction: (ssize_t) -> $492 ()(ii: ssize_t)
      reprep: (i : ssize_t) -> $492 ()(pretend-decreasingstd/core/undiv/pretend-decreasing: (x : ssize_t) -> $492 ssize_t(ii: ssize_t.incrstd/core/vector/ssize_t/incr: (i : ssize_t) -> $492 ssize_t))std/core/types/Unit: ()
  reprep: (i : ssize_t) -> $492 ()(0literal: int
dec  = 0
hex8 = 0x00
bit8 = 0b00000000.ssize_tstd/core/int/ssize_t: (i : int) -> $492 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) -> $434 maybe<$433> : (ssize_tstd/core/types/ssize_t: V) -> ee: E maybestd/core/types/maybe: V -> V<aa: V> )result: -> 485 maybe<484> : ee: E maybestd/core/types/maybe: V -> V<aa: V>
  fun reprep: (i : ssize_t) -> $434 maybe<$433>( ii: ssize_t : ssize_tstd/core/types/ssize_t: V )result: -> $434 maybe<$433>
    if ii: ssize_t <std/core/vector/ssize_t/(<): (ssize_t, ssize_t) -> $434 bool nn: ssize_t then
      match actionaction: (ssize_t) -> $434 maybe<$433>(ii: ssize_t)
        Nothingstd/core/types/Nothing: forall<a> maybe<a> -> reprep: (i : ssize_t) -> $434 maybe<$433>(pretend-decreasingstd/core/undiv/pretend-decreasing: (x : ssize_t) -> $434 ssize_t(ii: ssize_t.incrstd/core/vector/ssize_t/incr: (i : ssize_t) -> $434 ssize_t))
        Juststd/core/types/Just: forall<a> (value : a) -> maybe<a>(xx: $433) -> Juststd/core/types/Just: forall<a> (value : a) -> maybe<a>(xx: $433)
    else Nothingstd/core/types/Nothing: forall<a> maybe<a>
  reprep: (i : ssize_t) -> $434 maybe<$433>(0literal: int
dec  = 0
hex8 = 0x00
bit8 = 0b00000000.ssize_tstd/core/int/ssize_t: (i : int) -> $434 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)"