datatype 'a ralist with nat = Nil(0) | One(1) of 'a | {n:pos} Even (n+n) of 'a ralist(n) * 'a ralist(n) | {n:pos} Odd (n+n+1) of 'a ralist(n+1) * 'a ralist(n) (* suppose l1 = x1, ..., xn; l2 = y1, ..., yn; Even (l1, l2) = x1, y1, ..., xn, yn suppose l1 = x1, ..., xn, x; l2 = y1, ..., yn; Odd (l1, l2) = x1, y1, ..., xn, yn, x 1,2,3,4,5 Odd(Odd (Even(One(1), One(5)); One(3)); Even(One(2), One(4)) *) fun ('a) cons (x, xs) = case xs of Nil => One (x) | One (y) => Even (One(x), One(y)) | Even (xs', xs'') => Odd (cons (x, xs''), xs') | Odd (xs', xs'') => Even (cons (x, xs''), xs') withtype {n:nat} => 'a * 'a ralist(n) -> 'a ralist(n+1) fun ('a) uncons xs = case xs of One (x) => (x, Nil) | Even (xs', xs'') => let val (x, xs') = uncons xs' in (x, case xs' of Nil => xs'' | One _ => Odd (xs'', xs') | Even _ => Odd (xs'', xs') | Odd _ => Odd (xs'', xs')) end | Odd (xs', xs'') => let val (x, xs') = uncons xs' in (x, Even (xs'', xs')) end withtype {n:pos} => 'a ralist(n) -> 'a * 'a ralist(n-1) fun ('a) revApp (xs, ys) = case xs of Nil => ys | One x => cons (x, ys) | Even _ => let val (x, xs) = uncons xs in revApp (xs, cons (x, ys)) end | Odd _ => let val (x, xs) = uncons xs in revApp (xs, cons (x, ys)) end withtype {m:nat,n:nat} => 'a ralist(m) * 'a ralist(n) -> 'a ralist(m+n) fun ('a) reverse xs = revApp (xs, Nil) withtype {n:nat} <> => 'a ralist(n) -> 'a ralist(n) fun ('a) reverse Nil = Nil | reverse (One x) = One x | reverse (Even (xs, ys)) = Even (reverse ys, reverse xs) | reverse (Odd (xs, ys)) = Odd (reverse xs, reverse ys) withtype {n:nat} => 'a ralist(n) -> 'a ralist(n)