Team fight program written in twelf

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

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

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

sum: int -> int -> int -> type.
sum/0: sum X z X.
sum/1: sum X (s Y) (s Z)
	<- sum X Y Z.

sub: int -> int -> int -> type.
sub/0: sub X z X.
sub/1: sub (s X) (s Y) Z
	<- sub X Y Z.

name: type.
draw: name.
fighter: type.
nat: name -> int -> int -> fighter.

fight: fighter -> fighter -> name -> int -> type.
fight/0: fight (nat N1 A1 L1) (nat N2 A2 L2) N1 LL1
	<- L2 <= A1
	<- A2 < L1
	<- sub L1 A2 LL1.
fight/1: fight (nat N1 A1 L1) (nat N2 A2 L2) N2 LL2
	<- L1 <= A2
	<- A1 < L2
	<- sub L2 A1 LL2.
fight/2: fight (nat N1 A1 L1) (nat N2 A2 L2) draw 0
	<- L1 <= A2
	<- L2 <= A1.
fight/3: fight (nat N1 A1 L1) (nat N2 A2 L2) X Y
	<- A1 < L2
	<- A2 < L1
	<- sub L1 A2 LL1
	<- sub L2 A1 LL2
	<- fight (nat N1 A1 LL1) (nat N2 A2 LL2) X Y.

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

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

head: list -> fighter -> type.
head/0: head (X ; Y) X.

rest: list -> list -> type.
rest/0: rest (X ; Y) Y.

team: type.
t: name -> list -> team.

team_fight: team -> team -> team -> type.
team_fight/0: team_fight (t X *) (t Y *) (t draw *).
team_fight/1: team_fight (t N1 (T1 ; T2)) (t N2 *) (t N1 (T1 ; T2)).
team_fight/2: team_fight (t N1 *) (t N2 (T1 ; T2)) (t N2 (T1 ; T2)).
team_fight/3: team_fight (t N1 T1) (t N2 T2) (t N T)
	<- len T1 LT1
	<- 0 < LT1
	<- len T2 LT2
	<- 0 < LT2
	<- head T1 (nat NF1 NA1 NL1)
	<- head T2 (nat NF2 NA2 NL2)
	<- fight (nat NF1 NA1 NL1) (nat NF2 NA2 NL2) NF1 X
	<- rest T1 R1
	<- rest T2 R2
	<- team_fight (t N1 ((nat NF1 NA1 X) ; R1)) (t N2 R2) (t N T).
team_fight/4: team_fight (t N1 T1) (t N2 T2) (t N T)
	<- len T1 LT1
	<- 0 < LT1
	<- len T2 LT2
	<- 0 < LT2
	<- head T1 (nat NF1 NA1 NL1)
	<- head T2 (nat NF2 NA2 NL2)
	<- fight (nat NF1 NA1 NL1) (nat NF2 NA2 NL2) NF2 X
	<- rest T1 R1
	<- rest T2 R2
	<- team_fight (t N1 R1) (t N2 ((nat NF2 NA2 X) ; R2)) (t N T).
team_fight/5: team_fight (t N1 T1) (t N2 T2) (t N T)
	<- len T1 LT1
	<- 0 < LT1
	<- len T2 LT2
	<- 0 < LT2
	<- head T1 (nat NF1 NA1 NL1)
	<- head T2 (nat NF2 NA2 NL2)
	<- fight (nat NF1 NA1 NL1) (nat NF2 NA2 NL2) draw X
	<- rest T1 R1
	<- rest T2 R2
	<- team_fight (t N1 R1) (t N2 R2) (t N T).