// Path: src/main/java/ast/Expression.java
// public abstract class Expression implements Inferable<TypeInferenceEnv, Type> {
// 
//     @Override
//     public final Type infer() {
//         TypeInferenceEnv typeInferenceEnv = new TypeInferenceEnv();
//         Type t = infer(typeInferenceEnv);
// 
//         Substitution s = new Substitution();
// 
//         for (Constraint constraint : typeInferenceEnv.constraints()) {
//             s = constraint.apply(s).unify().composeWith(s);
//         }
// 
//         return t.apply(s);
//     }
// }
// 
// Path: src/main/java/exceptions/InfiniteTypeException.java
// public class InfiniteTypeException extends RuntimeException {
//     public InfiniteTypeException(Unifyable t1, Unifyable t2) {
//         super("This expression require an infinite type. (Trying to unify " + t1 + " and " +t2);
//     }
// }
// 
// Path: src/main/java/exceptions/UnboundVariableException.java
// public class UnboundVariableException extends RuntimeException {
//     public UnboundVariableException(Variable var) {
//         super("The variable '" + var.getName() + "' is not bound.");
//     }
// }
// 
// Path: src/main/java/exceptions/UnificationFailException.java
// public class UnificationFailException extends RuntimeException {
//     public UnificationFailException(Unifyable first, Unifyable second) {
//         super("The unification of inferred type for this expression has failed : " + first + " <=/=> " + second);
//     }
// }
// 
// Path: src/main/java/types/Type.java
// public abstract class Type extends Substitutable<Type> implements Unifyable{
// 
//     @Override
//     public Type identity() {
//         return this;
//     }
// 
//     @Override
//     public final Substitution unifyWith(Type type) {
//         if(this.equals(type)) return new Substitution();
//         if(type instanceof TVariable) return unifyWith((TVariable) type);
//         if(type instanceof TFunction) return unifyWith((TFunction) type);
//         if(type instanceof TConstructor) return unifyWith((TConstructor) type);
//         throw new UnificationFailException(this, type);
//     }
// 
//     protected Substitution unifyWith(TVariable var) {
//         return bind(var, this);
//     }
// 
//     protected Substitution unifyWith(TFunction fun) {
//         throw new UnificationFailException(this, fun);
//     }
// 
//     protected Substitution unifyWith(TConstructor cons) {
//         throw new UnificationFailException(this, cons);
//     }
// 
//     public abstract Type instantiate(Substitution sub);
// }


import ast.Expression;
import exceptions.InfiniteTypeException;
import exceptions.UnboundVariableException;
import exceptions.UnificationFailException;
import types.Type;
package app;


/**
 * Created by valentin on 25/10/2016.
 */
public class InferenceApp {
    static void infer(Expression exp) {
        try {
            Type t = exp.infer();
// Path: src/main/java/ast/Expression.java
// public abstract class Expression implements Inferable<TypeInferenceEnv, Type> {
// 
//     @Override
//     public final Type infer() {
//         TypeInferenceEnv typeInferenceEnv = new TypeInferenceEnv();
//         Type t = infer(typeInferenceEnv);
// 
//         Substitution s = new Substitution();
// 
//         for (Constraint constraint : typeInferenceEnv.constraints()) {
//             s = constraint.apply(s).unify().composeWith(s);
//         }
// 
//         return t.apply(s);
//     }
// }
// 
// Path: src/main/java/exceptions/InfiniteTypeException.java
// public class InfiniteTypeException extends RuntimeException {
//     public InfiniteTypeException(Unifyable t1, Unifyable t2) {
//         super("This expression require an infinite type. (Trying to unify " + t1 + " and " +t2);
//     }
// }
// 
// Path: src/main/java/exceptions/UnboundVariableException.java
// public class UnboundVariableException extends RuntimeException {
//     public UnboundVariableException(Variable var) {
//         super("The variable '" + var.getName() + "' is not bound.");
//     }
// }
// 
// Path: src/main/java/exceptions/UnificationFailException.java
// public class UnificationFailException extends RuntimeException {
//     public UnificationFailException(Unifyable first, Unifyable second) {
//         super("The unification of inferred type for this expression has failed : " + first + " <=/=> " + second);
//     }
// }
// 
// Path: src/main/java/types/Type.java
// public abstract class Type extends Substitutable<Type> implements Unifyable{
// 
//     @Override
//     public Type identity() {
//         return this;
//     }
// 
//     @Override
//     public final Substitution unifyWith(Type type) {
//         if(this.equals(type)) return new Substitution();
//         if(type instanceof TVariable) return unifyWith((TVariable) type);
//         if(type instanceof TFunction) return unifyWith((TFunction) type);
//         if(type instanceof TConstructor) return unifyWith((TConstructor) type);
//         throw new UnificationFailException(this, type);
//     }
// 
//     protected Substitution unifyWith(TVariable var) {
//         return bind(var, this);
//     }
// 
//     protected Substitution unifyWith(TFunction fun) {
//         throw new UnificationFailException(this, fun);
//     }
// 
//     protected Substitution unifyWith(TConstructor cons) {
//         throw new UnificationFailException(this, cons);
//     }
// 
//     public abstract Type instantiate(Substitution sub);
// }


// Path: src/main/java/app/InferenceApp.java
import ast.Expression;
import exceptions.InfiniteTypeException;
import exceptions.UnboundVariableException;
import exceptions.UnificationFailException;
import types.Type;

package app;


/**
 * Created by valentin on 25/10/2016.
 */
public class InferenceApp {
    static void infer(Expression exp) {
        try {
            Type t = exp.infer();
            System.out.println(exp + " :: " + t);