Random

Linear pseudo-random generators. Draws consume a generator and return a linear token containing the sample and its successor. Observe the sample with a borrowed *_value call, then consume the token with *_next or discard_draw / discard_int_draw / discard_range_draw. This prevents two projections from manufacturing aliases to one generator. An opaque pseudo-random generator (a Python `random.Random` at runtime), used linearly: every draw consumes it and produces a fresh successor. Being a `linear type`, every binder holding an `Rng` must be declared with multiplicity 1.
Imports
open Array;
Table of Contents

Types

Rng

(type) linear
An opaque pseudo-random generator (a Python `random.Random` at runtime), used linearly: every draw consumes it and produces a fresh successor. Being a `linear type`, every binder holding an `Rng` must be declared with multiplicity 1.
linear type Rng

Draw

(type) linear
Each result owns its successor generator until extracted or discarded.
linear type Draw

IntDraw

(type) linear
linear type IntDraw

RangeDraw

(type) linear
linear type RangeDraw

Functions

new_rng

A fresh generator seeded deterministically. The `Int` argument makes this an *applied* action, so each call yields a new generator — a nullary `def` would be a memoised value, aliasing one generator everywhere.
def new_rng (seed : Int) : Rng

draw

── Float draw in [0.0, 1.0) ────────────────────────────────────────────
def draw (1 g : Rng) : Draw

draw_value

def draw_value (borrow d : Draw) : {r : Float | r ≥ 0.0 && r < 1.0}

draw_next

def draw_next (1 d : Draw) : Rng

draw_int

── Integer draw in [lo, hi] ──────────────────────────────────────────── The bounds are repeated on the projection so the refinement survives the opaque `IntDraw`.
def draw_int (lo : Int) (hi : Int | hi ≥ lo) (1 g : Rng) : IntDraw

int_value

def int_value (lo : Int) (hi : Int | hi ≥ lo) (borrow d : IntDraw) : {r : Int | r ≥ lo && r ≤ hi}

int_next

def int_next (1 d : IntDraw) : Rng

draw_range

── Float draw in [lo, hi) ──────────────────────────────────────────────
def draw_range (lo : Float) (hi : Float | hi > lo) (1 g : Rng) : RangeDraw

range_value

def range_value (lo : Float) (hi : Float | hi > lo) (borrow d : RangeDraw) : {r : Float | r ≥ lo && r < hi}

range_next

def range_next (1 d : RangeDraw) : Rng

choose

── Uniform choice from a non-empty array (polymorphic) ─────────────────
def choose (1 xs : (Array a) | Array.size xs > 0) (1 g : Rng) : a

close_rng

Explicitly end ownership of a generator.
def close_rng (1 g : Rng) : Unit

discard_draw

End a draw chain after observing its final sample.
def discard_draw (1 d : Draw) : Unit

discard_int_draw

End a draw chain after observing its final sample.
def discard_int_draw (1 d : IntDraw) : Unit

discard_range_draw

End a draw chain after observing its final sample.
def discard_range_draw (1 d : RangeDraw) : Unit