polymorphic_higher_order.elf

obj: type.
int: obj.
t: obj -> type. %postfix 1 t.
z: int t.
s: int t -> int t.

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

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

eval: T t -> T t -> type.

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

mult: int t -> int t -> int t.
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: obj -> obj. %postfix 1 list.
*: T list t.
;: T t -> T list t -> T list t. %infix right 1 ;.

fold_aux: (T t -> T t -> T t) -> T list t -> T t.
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: (T t -> T t -> T t) -> T t -> T list t -> T t.
fold/0: eval (fold Func Acc Xs) Y
	<- eval (fold_aux Func (Acc ; Xs)) Y.


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