Skip to content

Commit

Permalink
parameterized IndexedArrayFun contract.
Browse files Browse the repository at this point in the history
  • Loading branch information
Ben Yang committed Feb 6, 2024
1 parent 9cc56a5 commit 4677b57
Showing 1 changed file with 15 additions and 8 deletions.
23 changes: 15 additions & 8 deletions core/stdlib/std.ncl
Original file line number Diff line number Diff line change
Expand Up @@ -159,7 +159,7 @@

at
: forall a. Number -> Array a -> a
| std.contract.unstable.IndexedArrayFun
| std.contract.unstable.IndexedArrayFun 'Index
| doc m%"
Retrieves the n-th element from an array, with indices starting at 0.

Expand Down Expand Up @@ -570,7 +570,7 @@

split_at
: forall a. Number -> Array a -> { left : Array a, right : Array a }
| std.contract.unstable.IndexedArrayFun
| std.contract.unstable.IndexedArrayFun 'Split
| doc m%"
Splits an array in two at a given index and puts all the elements
to the left of the element at the given index (excluded) in the
Expand Down Expand Up @@ -1358,11 +1358,12 @@
value
in

let ArrayIndexSecond = fun min_size label value =>
let ArrayIndexSecond = fun type min_size label value =>
if %typeof% min_size == 'Number && %typeof% value == 'Array then
if min_size >= %length% value then
let max_idx = type |> match { 'Index => %length% value - 1, 'Split => %length% value } in
if min_size > max_idx then
let index_as_str = %to_str% min_size in
let max_as_str = %to_str% (%length% value) in
let max_as_str = %to_str% max_idx in
let note =
if %length% value == 0 then
"Can't index into an empty array"
Expand All @@ -1378,9 +1379,15 @@
else
value
in
DependentFun
ArrayIndexFirst
(fun index => ArrayIndexSecond index -> Dyn),
let contract
| [| 'Index, 'Split |] -> Dyn -> Dyn
= fun type label function =>
DependentFun
ArrayIndexFirst
(fun index => ArrayIndexSecond type index -> Dyn)
label
function
in contract,

ArraySliceFun
| doc m%"
Expand Down

0 comments on commit 4677b57

Please sign in to comment.