mergesort.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.

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

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

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

len: list -> int -> type.
len/0: len * 0.
len/1: len (X ; Xs) (s Y)
	<- len Xs Y.

sub_reverse: list -> list -> list -> type.
sub_reverse/0: sub_reverse * X X.
sub_reverse/1: sub_reverse (X ; Xs) Y Z
	<- sub_reverse Xs (X ; Y) Z.

reverse: list -> list -> type.
reverse/0: reverse X Y
	<- sub_reverse X * Y.

sub_split: list -> list -> list -> list -> type.
sub_split/0: sub_split (X ; Xs) Y Z1 Z2
	<- len (X ; Xs) XLEN
	<- len Y YLEN
	<- YLEN < XLEN
	<- sub_split Xs (X ; Y) Z1 Z2.
sub_split/1: sub_split X Y X Y1
	<- len X XLEN
	<- len Y YLEN
	<- XLEN <= YLEN
	<- reverse Y Y1.

split: list -> list -> list -> type.
split/0: split X Y Z
	<- sub_split X * Y Z.

merge: list -> list -> list -> type.
merge/0: merge * * *.
merge/1: merge X * X
	<- len X XLEN
	<- 0 < XLEN.
merge/2: merge * X X
	<- len X XLEN
	<- 0 < XLEN.
merge/3: merge (X ; Xs) (Y ; Ys) (X ; Z)
	<- X < Y
	<- merge Xs (Y ; Ys) Z.
merge/4: merge (X ; Xs) (Y ; Ys) (Y ; Z)
	<- Y <= X
	<- merge (X ; Xs) Ys Z.

mergesort: list -> list -> type.
mergesort/0: mergesort (X ; *) (X ; *).
mergesort/1: mergesort X Y
	<- split X X1 X2
	<- mergesort X1 Y1
	<- mergesort X2 Y2
	<- merge Y1 Y2 Y.