// Featherweight Java examples

// simulating naturals in FJ using Church numerals
//  (call-by-name Church numerals)
//  zero = \s.\z.z
//  one = \s.\z.s z
//  two = \s.\z.s (s z)
//  three = \s.\z.s (s (s z))
//  succ = \n.\s.\z.s (n s z)
//  succ = \n.\s.\z.n s (s z)
//  plus = \n.\m.\s.\z. n s (m s z)
//  plus = \n.\m.n succ (m succ zero)
//  n succ zero = n

//  the cleanest way to implement Church numerals
//  is to implement Lambda calculus, and then to
//  translate directly

class Function extends Object {
    Object apply(Object arg) { return new Object(); }  // abstract
}

class Nat extends Object {
    Object eval(Function s, Object z) { return new Object(); }  // abstract
}

class Zero extends Nat {
    Zero() { super(); }
    Object eval(Function s, Object z) { return z; }
}

class Succ extends Nat {
    Nat n;
    Succ(Nat n) { super(); this.n = n; }
    Object eval(Function s, Object z) { return s.apply(n.eval(s, z)); }
}

class Plus extends Nat {
    Nat m;
    Nat n;
    Plus(Nat m, Nat n) { super(); this.m = m; this.n = n; }
    Object eval(Function s, Object z) { return m.eval(s, n.eval(s, z)); }
}

class SuccFunction extends Function {
    SuccFunction() { super(); }
    Object apply(Object arg) { return new Integer(1+(Integer)arg); }
}

class Feath3 {
    static Integer toInteger(Nat n) {
	return (Integer)n.eval(new SuccFunction(), new Integer(0));
    }
    public static void main(String[] args) {
	Nat n = new Plus(new Succ(new Succ(new Succ(new Zero()))),
			 new Succ(new Succ(new Zero())));
	System.out.println(toInteger(n));
    }
}