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

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

eval: int -> int -> type.

add: int -> int -> int.
add/0: eval (add 0 X) X.
add/1: eval (add (s X) Y) (s Z)
	<- eval (add X Y) Z.

mult: int -> int -> int.
mult/0: eval (mult 0 X) 0.
mult/1: eval (mult 1 X) X.
mult/1: eval (mult (s X) Y) Z
	<- 0 < X
	<- eval (add Y Z1) Z
	<- eval (mult X Y) Z1.

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

fold_aux: (int -> int -> int) -> list -> int.
fold_aux/0: eval (fold_aux Func (X ; *)) X.
fold_aux/1: eval (fold_aux Func (X1 ; X2 ; Xs)) Y
	<- eval (Func X1 X2) X
	<- eval (fold_aux Func (X ; Xs)) Y.

fold: (int -> int -> int) -> int -> list -> int.
fold/0: eval (fold Func Acc Xs) Y
	<- eval (fold_aux Func (Acc ; Xs)) Y.


equation = fold mult 1 (1 ; 2 ; 3 ; 4 ; *).