No matching definitions.

tur/range-bound

stdlib/range-bound.tur

Bound A GADT: typed range endpoints (R3).

Since: stdlib-refinement-collections-plan (R3)

defn

bound-inclusive

(bound-inclusive [v : int] :)

construct an inclusive endpoint at v.

vthe endpoint value (part of the interval)

A (Bound int) tagged Inclusive.

(range-contains? (bound-range (bound-inclusive 1) (bound-unbounded)) 1)  ; => true

Since: R3

defn

bound-exclusive

(bound-exclusive [v : int] :)

construct an exclusive endpoint at v.

vthe open boundary value (not part of the interval)

A (Bound int) tagged Exclusive.

(range-contains? (bound-range (bound-inclusive 1) (bound-exclusive 5)) 5)  ; => false

Since: R3

defn

bound-unbounded

(bound-unbounded :)

construct an unbounded (open-ended) endpoint.

A (Bound int) tagged Unbounded.

(range-contains? (bound-range (bound-unbounded) (bound-unbounded)) 999)  ; => true

Since: R3

defn

bound->range-bound

(bound->range-bound [b : Bound] :)

deprecated compatibility shim (now near-identity).

bthe (Bound int)

The same (Bound int), accepted by range-new and every range.tur predicate.

(range-bound-inclusive? (bound->range-bound (bound-inclusive 3)))  ; => true

Since: R3

defn

range-bound->bound

(range-bound->bound [b : Bound] :)

deprecated compatibility shim (now near-identity).

ba (Bound int)

The same (Bound int).

(bound-value (range-bound->bound (range-lower (closed-range 2 8))))  ; => 2

Since: R3

defn

bound-value

(bound-value [b : Bound] :)

extract the endpoint value from a bounded endpoint.

ba (Bound int); Unbounded yields 0

The endpoint value for Inclusive / Exclusive, or 0 for Unbounded.

(bound-value (bound-exclusive 7))  ; => 7

Since: R3

defn

bound-inclusive?

(bound-inclusive? [b : Bound] :)

true when an endpoint is inclusive.

ba (Bound int)

true for Inclusive, false for Exclusive or Unbounded.

(bound-inclusive? (bound-inclusive 1))  ; => true

Since: R3

defn

bound-range

(bound-range [lo : Bound hi : Bound] :)

build a Range from two GADT endpoints.

lothe lower (Bound int)
hithe upper (Bound int)

An :int Range pointer, usable with every range.tur predicate.

(range-contains? (bound-range (bound-inclusive 1) (bound-exclusive 5)) 4)  ; => true

Since: R3

defn

range-lower-bound

(range-lower-bound [r : int] :)

the lower endpoint of a Range as a Bound GADT.

ran :int Range pointer

The lower endpoint lifted into the (Bound int) GADT.

(bound-inclusive? (range-lower-bound (closed-range 1 5)))  ; => true

Since: R3

defn

range-upper-bound

(range-upper-bound [r : int] :)

the upper endpoint of a Range as a Bound GADT.

ran :int Range pointer

The upper endpoint lifted into the (Bound int) GADT.

(bound-unbounded? (range-upper-bound (at-least-range 3)))  ; => true

Since: R3

defn

range-fmt

(range-fmt [lo-kind : int lo-val : int hi-kind : int hi-val : int] :)
defn

bound-kind

(bound-kind [b : Bound] :)
defn

range->str

(range->str [r : int] :)

render a Range in interval notation.

ran :int Range pointer

A freshly allocated :cstr interval string.

(range->str (closed-open-range 1 5))  ; => "[1, 5)"
  (range->str (at-most-range 5))        ; => "(-inf, 5]"

Since: range-gadt-typeclass-migration-plan B2

defn

bound->str

(bound->str [b : Bound] :)

render a single Bound endpoint.

ba (Bound int)

A freshly allocated :cstr.

(bound->str (bound-inclusive 3))  ; => "[3"
  (bound->str (bound-unbounded))    ; => "unbounded"

Since: range-gadt-typeclass-migration-plan B2

defn

bound-fmt

(bound-fmt [kind : int v : int] :)