@@ -591,34 +591,6 @@ def i_to_n(x:Int) -> Maybe Nat =
591591 then Nothing
592592 else Just $ unsafe_i_to_n x
593593
594- '## Fencepost index sets
595-
596- struct Post(segment:Type) =
597- val : Nat
598-
599- instance Ix(Post segment) given (segment|Ix)
600- def size'() = size segment + 1
601- def ordinal(i) = i.val
602- def unsafe_from_ordinal(i) = Post(i)
603-
604- def left_post(i:n) -> Post n given (n|Ix) =
605- unsafe_from_ordinal(n=Post n, ordinal i)
606-
607- def right_post(i:n) -> Post n given (n|Ix) =
608- unsafe_from_ordinal(n=Post n, ordinal i + 1)
609-
610- interface NonEmpty(n|Ix)
611- first_ix : n
612-
613- def last_ix() ->> n given (n|NonEmpty) =
614- unsafe_from_ordinal(unsafe_i_to_n(n_to_i(size n) - 1))
615-
616- instance NonEmpty(Post n) given (n|Ix)
617- first_ix = unsafe_from_ordinal(n=Post n, 0)
618-
619- instance NonEmpty(())
620- first_ix = unsafe_from_ordinal(0)
621-
622594'### Monoid
623595A [monoid](https://en.wikipedia.org/wiki/Monoid) is a things that have an associative binary operator and an identity element.
624596This is a very useful and general calls of things.
@@ -901,6 +873,12 @@ instance Ix(Maybe a) given (a|Ix)
901873 False -> Just $ unsafe_from_ordinal o
902874 True -> Nothing
903875
876+ interface NonEmpty(n|Ix)
877+ first_ix : n
878+
879+ instance NonEmpty(())
880+ first_ix = unsafe_from_ordinal(0)
881+
904882instance NonEmpty(Bool)
905883 first_ix = unsafe_from_ordinal 0
906884
@@ -918,6 +896,40 @@ instance NonEmpty(Either(a,b)) given (a|NonEmpty, b|Ix)
918896instance NonEmpty(Maybe a) given (a|Ix)
919897 first_ix = unsafe_from_ordinal 0
920898
899+ '## Fencepost index sets
900+
901+ struct Post(segment:Type) =
902+ val : Nat
903+
904+ instance Ix(Post segment) given (segment|Ix)
905+ def size'() = size segment + 1
906+ def ordinal(i) = i.val
907+ def unsafe_from_ordinal(i) = Post(i)
908+
909+ def left_post(i:n) -> Post n given (n|Ix) =
910+ unsafe_from_ordinal(n=Post n, ordinal i)
911+
912+ def right_post(i:n) -> Post n given (n|Ix) =
913+ unsafe_from_ordinal(n=Post n, ordinal i + 1)
914+
915+ def left_fence(p:Post n) -> Maybe n given (n|Ix) =
916+ ix = ordinal p
917+ if ix == 0
918+ then Nothing
919+ else Just $ unsafe_from_ordinal $ ix -| 1
920+
921+ def right_fence(p:Post n) -> Maybe n given (n|Ix) =
922+ ix = ordinal p
923+ if ix == size n
924+ then Nothing
925+ else Just $ unsafe_from_ordinal ix
926+
927+ def last_ix() ->> n given (n|NonEmpty) =
928+ unsafe_from_ordinal(unsafe_i_to_n(n_to_i(size n) - 1))
929+
930+ instance NonEmpty(Post n) given (n|Ix)
931+ first_ix = unsafe_from_ordinal(n=Post n, 0)
932+
921933def scan(
922934 init:a,
923935 body:(n, a)->(a,b)
@@ -2016,27 +2028,45 @@ instance Arbitrary(Fin n) given (n)
20162028
20172029'### Searching
20182030
2019- 'returns the highest index `i` such that `xs.i <= x`
2031+ 'Returns the bucket of `x` assuming boundaries `xs` as a `Post n`.
2032+ The boundaries must already be sorted, and are inclusive on the left.
2033+
2034+ 'In other words, if there is an index `i` such that `xs.i <= x`,
2035+ returns the `right_post` of the highest such index; otherwise returns
2036+ `first_ix : Post n`, which is also the `left_post` of the minimum `i`.
20202037
2021- def search_sorted(xs:n=>a, x:a) -> Maybe n given (n|Ix, a|Ord) =
2038+ 'This is equivalent to the right-biased formulation: if an index `i`
2039+ exists such that `x < xs.i`, returns the `left_post` of the least such
2040+ `i`, otherwise returns `last_ix : Post n`, i.e., the `right_post` of
2041+ the maximum `i`.
2042+
2043+ def search_sorted(xs:n=>a, x:a) -> Post n given (n|Ix, a|Ord) =
20222044 if size n == 0
2023- then Nothing
2045+ then first_ix
20242046 else if x < xs[from_ordinal 0]
2025- then Nothing
2047+ then first_ix
20262048 else
20272049 low <- with_state(0)
20282050 high <- with_state(size n)
20292051 _ <- iter
20302052 numLeft = n_to_i (get high) - n_to_i (get low)
20312053 if numLeft == 1
2032- then Done $ Just $ from_ordinal $ get low
2054+ then Done $ right_post $ from_ordinal $ get low
20332055 else
20342056 centerIx = get low + unsafe_i_to_n (numLeft `idiv` 2)
20352057 if x < xs[from_ordinal centerIx]
20362058 then high := centerIx
20372059 else low := centerIx
20382060 Continue
20392061
2062+ 'If `i` exists such that `xs.i == x`, returns `Just` of the largest
2063+ such `i`, otherwise returns `Nothing`.
2064+
2065+ def search_sorted_exact(xs:n=>a, x:a) -> Maybe n given (n|Ix, a|Ord) =
2066+ case left_fence(search_sorted(xs, x)) of
2067+ Just i -> if xs[i] == x then Just i else Nothing
2068+ Nothing -> Nothing
2069+
20402070'### min / max etc
20412071
20422072def min_by(f:(a)->o, x:a, y:a) -> a given (o|Ord, a) = select(f x < f y, x, y)
@@ -2318,8 +2348,7 @@ def lines(source:String) -> List String =
23182348-- cdf should include 0.0 but not 1.0
23192349def categorical_from_cdf(cdf: n=>Float, key: Key) -> n given (n|Ix) =
23202350 r = rand key
2321- case search_sorted(cdf, r) of
2322- Just(i) -> i
2351+ from_just $ left_fence $ search_sorted(cdf, r)
23232352
23242353def normalize_pdf(xs: d=>Float) -> d=>Float given (d|Ix) = xs / sum xs
23252354
0 commit comments