import java.util.TreeMap;

public class JavaExample
{

    public static void main(String [] args)
    {
        TreeMap<String, Type> xNatural = new TreeMap<String, Type>();
        xNatural.put("x", new Natural());

        TreeMap<String, Term> xZeroYOne = new TreeMap<String, Term>();
        xZeroYOne.put("x", new Number(0));
        xZeroYOne.put("y", new Number(1));

        Term term = new Application(new Abstraction("r", new RecordType(xNatural), new Projection(new Variable("r"), "x")), new Record(xZeroYOne));

        Type type = term.typecheck(new TreeMap<String, Type>());
    }

}

abstract class Term {
    abstract Type typecheck(TreeMap<String, Type> context);
}

class Variable extends Term {
    String name;

    Variable(String name) {
        this.name = name;
    }

    Type typecheck(TreeMap<String, Type> context) {
        throw new UnsupportedOperationException();
    }
}

class Abstraction extends Term {
    String variableName;
    Type variableType;
    Term body;

    Abstraction(String variableName, Type variableType, Term body) {
        this.variableName = variableName;
        this.variableType = variableType;
        this.body = body;
    }

    Type typecheck(TreeMap<String, Type> context) {
        throw new UnsupportedOperationException();
    }
}

class Application extends Term {
    Term function;
    Term argument;

    Application(Term function, Term argument) {
        this.function = function;
        this.argument = argument;
    }

    Type typecheck(TreeMap<String, Type> context) {
        throw new UnsupportedOperationException();
    }
}

class Record extends Term {
    TreeMap<String, Term> fields;

    Record(TreeMap<String, Term> fields) {
        this.fields = fields;
    }

    Type typecheck(TreeMap<String, Type> context) {
        throw new UnsupportedOperationException();
    }
}

class Projection extends Term {
    Term term;
    String label;

    Projection(Term term, String label) {
        this.term = term;
        this.label = label;
    }

    Type typecheck(TreeMap<String, Type> context) {
        throw new UnsupportedOperationException();
    }
}

class Number extends Term {
    Integer value;

    Number(Integer value) {
        this.value = value;
    }

    Type typecheck(TreeMap<String, Type> context) {
        throw new UnsupportedOperationException();
    }
}


abstract class Type {
}

class Top extends Type {
    Top() {
    }
}

class FunctionType extends Type {
    Type argumentType;
    Type resultType;

    FunctionType(Type argumentType, Type resultType) {
        this.argumentType = argumentType;
        this.resultType = resultType;
    }
}

class RecordType extends Type {
    TreeMap<String, Type> fieldTypes;

    RecordType(TreeMap<String, Type> fieldTypes){
        this.fieldTypes = fieldTypes;
    }
}

class Natural extends Type {
    Natural(){
    }
}