random.egi

--
--
-- Random
--
--

def rands (s: Integer) (e: Integer) : [Integer] := pureRand s e :: rands s e

def pureRand (s: Integer) (e: Integer) : Integer := io (rand s e)

def randomize {Eq a} (xs: [a]) : [a] :=
  let randomize' xs n :=
        if n = 0
          then []
          else let r := pureRand 1 n
                   x := nth r xs
                in x :: randomize' (deleteFirst x xs) (n - 1)
   in randomize' xs (length xs)

def R.between (s: Integer) (e: Integer) : [Integer] := randomize [s..e]

def R.multiset {a} (m: Matcher a) : Matcher [a] :=
  matcher
    | [] as () with
      | [] -> [()]
      | _ -> []
    | $ :: $ as (m, R.multiset m) with
      | $tgt ->
        map
          (\i ->
            match tgt as list m with
              | loop $j (1, i - 1, _)
                  ($xa_j :: ...)
                  ($x :: $ts) ->
                (x, map (\j -> xa_j) [1..(i - 1)] ++ ts))
          (R.between 1 (length tgt))
    | $ as (something) with
      | $tgt -> [tgt]

def R.uncons {a} (xs: [a]) : (a, [a]) :=
  head
    (matchAll xs as R.multiset something with
      | $x :: $rs -> (x, rs))

def R.head {a} (xs: [a]) : a :=
  head
    (matchAll xs as R.multiset something with
      | $x :: _ -> x)

def R.tail {a} (xs: [a]) : [a] :=
  head
    (matchAll xs as R.multiset something with
      | _ :: $rs -> rs)

def sample {a} : [a] -> a := R.head

def R.set {a} (m: Matcher a) : Matcher [a] :=
  matcher
    | [] as () with
      | [] -> [()]
      | _ -> []
    | $ :: $ as (m, R.multiset m) with
      | $tgt ->
        map
          (\i ->
            match tgt as list m with
              | loop $j (1, i - 1, _)
                  (_ :: ...)
                  ($x :: _) -> (x, tgt))
          (R.between 1 (length tgt))
    | $ as (something) with
      | $tgt -> [tgt]

def f.rands (s: Float) (e: Float) : [Float] := f.pureRand s e :: f.rands s e

def f.pureRand (s: Float) (e: Float) : Float := io (f.rand s e)