/*---------------------------------------------------------------------------
  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).value[#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: $232 : 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) -> $261 : 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<$284> : vectorstd/core/types/vector: V -> V<aa: V>, ^indexindex: int : intstd/core/types/int: V )result: -> exn 338 : 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<$284>.lengthzstd/core/vector/lengthz: (v : vector<$284>) -> exn ssize_t then unsafe-idxstd/core/vector/unsafe-idx: (v : vector<$284>, index : ssize_t) -> exn $284(vv: vector<$284>,idxidx: ssize_t) else throwstd/core/exn/throw: (message : string, info : ? exception-info) -> exn $284("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<$343> : vectorstd/core/types/vector: V -> V<aa: V>, ^indexindex: int : intstd/core/types/int: V )result: -> total maybe<391> : 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<$343>.lengthzstd/core/vector/lengthz: (v : vector<$343>) -> ssize_t then Juststd/core/types/Just: forall<a> (value : a) -> maybe<a>(unsafe-idxstd/core/vector/unsafe-idx: (v : vector<$343>, index : ssize_t) -> $343(vv: vector<$343>,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<$396> : vectorstd/core/types/vector: V -> V<aa: V> )result: -> total int : intstd/core/types/int: V
  vv: vector<$396>.lengthzstd/core/vector/lengthz: (v : vector<$396>) -> 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: $420 : aa: V)result: -> total vector<441> : vectorstd/core/types/vector: V -> V<aa: V>
  vector-allocstd/core/vector/vector-alloc: (n : ssize_t, init : $420) -> vector<$420>(nn: int.ssize_tstd/core/int/ssize_t: (i : int) -> ssize_t, defaultdefault: $420)

// 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) -> $446 : intstd/core/types/int: V -> astd/core/types/total: E )result: -> total vector<476> : vectorstd/core/types/vector: V -> V<aa: V>
  vector-alloc-totalstd/core/vector/vector-alloc-total: (n : ssize_t, f : (ssize_t) -> $446) -> vector<$446>( nn: int.ssize_tstd/core/int/ssize_t: (i : int) -> ssize_t, fnfn: (i : ssize_t) -> $446(ii: ssize_t) ff: (int) -> $446(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) -> $544 $543 : intstd/core/types/int: V -> ee: E aa: V )result: -> 592 vector<591> : ee: E vectorstd/core/types/vector: V -> V<aa: V>
  val lenlen: ssize_t = nn: int.ssize_tstd/core/int/ssize_t: (i : int) -> $544 ssize_t
  val vv: vector<$543> = unsafe-vectorstd/core/vector/unsafe-vector: (n : ssize_t) -> $544 vector<$543>(lenlen: ssize_t)
  forzstd/core/vector/forz: (n : ssize_t, action : (ssize_t) -> $544 ()) -> $544 ()( lenlen: ssize_t ) fnfn: (i : ssize_t) -> $544 ()(ii: ssize_t)
    unsafe-assignstd/core/vector/unsafe-assign: (v : vector<$543>, i : ssize_t, x : $543) -> $544 ()(vv: vector<$543>,ii: ssize_t,ff: (int) -> $544 $543(ii: ssize_t.intstd/core/int/ssize_t/int: (i : ssize_t) -> $544 int))
  vv: vector<$543>

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

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

fun foreach-indexedzstd/core/vector/foreach-indexedz: forall<a,e> (v : vector<a>, f : (ssize_t, a) -> e ()) -> e ()( vv: vector<$599> : vectorstd/core/types/vector: V -> V<aa: V>, ff: (ssize_t, $599) -> $600 () : (ssize_tstd/core/types/ssize_t: V,aa: V) -> ee: E (std/core/types/unit: V)std/core/types/unit: V )result: -> 637 () : ee: E (std/core/types/unit: V)std/core/types/unit: V
  forzstd/core/vector/forz: (n : ssize_t, action : (ssize_t) -> $600 ()) -> $600 ()( vv: vector<$599>.lengthzstd/core/vector/lengthz: (v : vector<$599>) -> $600 ssize_t ) fnfn: (i : ssize_t) -> $600 ()(ii: ssize_t)
    ff: (ssize_t, $599) -> $600 ()(ii: ssize_t,vv: vector<$599>.unsafe-idxstd/core/vector/unsafe-idx: (v : vector<$599>, index : ssize_t) -> $600 $599(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<$787> : vectorstd/core/types/vector: V -> V<aa: V>, ff: ($787) -> $789 maybe<$788> : aa: V -> ee: E maybestd/core/types/maybe: V -> V<bb: V> )result: -> 833 maybe<832> : ee: E maybestd/core/types/maybe: V -> V<bb: V>
  for-whilezstd/core/vector/for-whilez: (n : ssize_t, action : (ssize_t) -> $789 maybe<$788>) -> $789 maybe<$788>( vv: vector<$787>.lengthzstd/core/vector/lengthz: (v : vector<$787>) -> $789 ssize_t ) fnfn: (i : ssize_t) -> $789 maybe<$788>(ii: ssize_t)
    ff: ($787) -> $789 maybe<$788>(vv: vector<$787>.unsafe-idxstd/core/vector/unsafe-idx: (v : vector<$787>, index : ssize_t) -> $789 $787(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<$843> : vectorstd/core/types/vector: V -> V<aa: V>, ff: ($843) -> $845 $844 : aa: V -> ee: E bb: V )result: -> 903 vector<902> : ee: E vectorstd/core/types/vector: V -> V<bb: V>
  val ww: vector<$844> = unsafe-vectorstd/core/vector/unsafe-vector: (n : ssize_t) -> $845 vector<$844>(vv: vector<$843>.lengthstd/core/vector/length: (v : vector<$843>) -> $845 int.ssize_tstd/core/int/ssize_t: (i : int) -> $845 ssize_t)
  vv: vector<$843>.foreach-indexedzstd/core/vector/foreach-indexedz: (v : vector<$843>, f : (ssize_t, $843) -> $845 ()) -> $845 () fnfn: (i : ssize_t, x : $843) -> $845 ()(ii: ssize_t,xx: $843)
    unsafe-assignstd/core/vector/unsafe-assign: (v : vector<$844>, i : ssize_t, x : $844) -> $845 ()(ww: vector<$844>,ii: ssize_t,ff: ($843) -> $845 $844(xx: $843))
  ww: vector<$844>

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

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

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