qsort.elf

int: type.
z: int.
s: int -> int.

0 = z.
1 = s 0.
2 = s 1.
3 = s 2.
4 = s 3.
5 = s 4.
6 = s 5.
7 = s 6.
8 = s 7.
9 = s 8.
10 = s 9.

<: int -> int -> type. %infix none 1 <.
</0: X < (s X).
</1: X < (s Y)
	<- X < Y.
%mode < +X +Y.

<>: int -> int -> type. %infix none 1 <>.
<>/0: X <> Y
	<- X < Y.
<>/1: X <> Y
	<- Y < X.
%mode <> +X +Y.

<=: int -> int -> type. %infix none 1 <=.
<=/0: X <= X.
<=/1: X <= Y
	<- X < Y.
%mode <= +X +Y.

list: type.
*: list.
;: int -> list -> list. %infix right 1 ;.

len: list -> int -> type.
len/0: len * 0.
len/1: len (X ; XS) (s Y)
	<- len XS Y.
%mode len +X -Y.

reverse: list -> list -> list -> type.
reverse/0: reverse * X X.
reverse/1: reverse (X ; XS) Y Z
	<- reverse XS (X ; Y) Z.
%mode reverse +X +Y -Z.

concat: list -> list -> list -> type.
concat/0: concat * X X.
concat/1: concat X Y Z
	<- reverse X * (X1 ; XS)
	<- reverse XS * XS1
	<- concat XS1 (X1 ; Y) Z.
%mode concat +X +Y -Z.

less: list -> int -> list -> type.
less/0: less * X *.
less/1: less (X ; XS) Y (X ; Z)
	<- X < Y
	<- less XS Y Z.
less/2: less (X ; XS) Y Z
	<- Y <= X
	<- less XS Y Z.
%mode less +X +Y -Z.

more: list -> int -> list -> type.
more/0: more * X *.
more/1: more (X ; XS) Y (X ; Z)
	<- Y < X
	<- more XS Y Z.
more/2: more (X ; XS) Y Z
	<- X <= Y
	<- more XS Y Z.
%mode more +X +Y -Z.

same: list -> int -> list -> type.
same/0: same * X *.
same/1: same (X ; XS) X (X ; Z)
	<- same XS X Z.
same/2: same (X ; XS) Y Z
	<- X <> Y
	<- same XS Y Z.
%mode same +X +Y -Z.

qsort: list -> list -> type.
qsort/0: qsort * *.
qsort/1: qsort (X ; *) (X ; *).
qsort/2: qsort (X ; XS) Y
	<- len (X ; XS) LEN
	<- 1 < LEN
	<- less (X ; XS) X L
	<- same (X ; XS) X S
	<- more (X ; XS) X M
	<- qsort L L1
	<- qsort S S1
	<- qsort M M1
	<- concat L1 S1 Y1
	<- concat Y1 M1 Y.
%mode qsort +X -Y.