--
--
-- Random
--
--

def rands s e := pureRand s e :: rands s e

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

def randomize xs :=
  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 e := randomize [s..e]

def R.multiset a :=
  matcher
    | [] as () with
      | [] -> [()]
      | _ -> []
    | $ :: $ as (a, R.multiset a) with
      | $tgt ->
        map
          (\i ->
            match tgt as list a 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 xs :=
  head
    (matchAll xs as R.multiset something with
      | $x :: $rs -> (x, rs))

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

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

def sample := R.head

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

def f.rands s e := f.pureRand s e :: f.rands s e

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