1	import Base
2	import ../../../src/math/u64.bend as W
3	
4	# What a source (the Source interface of src/math/random/rand.bend: a state
5	# type S and a step ~next: S -> W.U64 & S) is observed to do: the sequence of
6	# its outputs. Two sources with the same outputs are the same generator for
7	# every function of rand.bend.
8	
9	def fst64(-S: Data, p: W.U64 & S) -> W.U64:
10	  (x, s) = p
11	  x
12	
13	def snd64(-S: Data, p: W.U64 & S) -> S:
14	  (x, s) = p
15	  s
16	
17	# the first n outputs of the source from state s
18	def outputs(~S: Data, ~next: S -> W.U64 & S, n: Nat, +s: S) -> List<&2, W.U64>:
19	  match n:
20	    case 0n:
21	      []
22	    case 1n+p:
23	      Con{fst64(S, next(s)), outputs(~S, ~next, p, snd64(S, next(s)))}