object TypeCheck {

  def typeOf(e: ExprExt, nv: List[TBind], tnv: List[TVBind]): Type = {
  //println("e: " + e + " nv: " + nv + " tnv: " + tnv)
    e match {
      case NumExt(n) => NumT()
      case PlusExt(e1, e2) =>
        (normalizeType(typeOf(e1, nv, tnv),tnv), normalizeType(typeOf(e2, nv, tnv),tnv)) match {
          case (NumT(), NumT()) =>
            NumT()
          case r =>
            throw TypeException("expected both branches of plus expression to be num typed, but got: " + r)
        }
      case MultExt(e1, e2) =>
        (normalizeType(typeOf(e1, nv, tnv),tnv), normalizeType(typeOf(e2, nv, tnv),tnv)) match {
          case (NumT(), NumT()) =>
            NumT()
          case r =>
            throw TypeException("expected both branches of mult expression to be num typed, but got: " + r)
        }
      case FdExt(x, t, e) => {
        val nv2 = TBind(x,normalizeType(t,tnv))::nv
        FunT(normalizeType(t,tnv), normalizeType(typeOf(e,nv2,tnv),tnv))
      }
      case AppExt(f, a) => normalizeType(typeOf(f,nv,tnv),tnv) match {
        case FunT(in,out) => if(normalizeType(typeOf(a,nv,tnv),tnv)==normalizeType(in,tnv)) out else throw TypeException("wrong input for function app")
        case _ => throw TypeException("no function in app")
      }
      case IdExt(x) => normalizeType(lookup(x, nv),tnv) match {
        case VarT(a) => normalizeType(VarT(a),tnv)
        case b => normalizeType(b,tnv)
      }
      case ConsExt(hd, tl) => {
        val t = normalizeType(typeOf(hd,nv,tnv),tnv)
        if(t==normalizeType(typeOf(tl,nv,tnv),tnv)) ListT(normalizeType(t,tnv))
        else if (ListT(t)==normalizeType(typeOf(tl,nv,tnv),tnv)) ListT(normalizeType(t,tnv))
        else {
          println("cons: " + t + " " + typeOf(tl,nv,tnv))
          throw TypeException("not same types in list")
        }
      }
      case NilExt(t) => ListT(normalizeType(t,tnv))
      case HeadExt(e) => normalizeType(typeOf(e,nv,tnv),tnv) match {
       case ListT(x) => normalizeType(x,tnv)
       case _ => throw TypeException("head not a list")
      }
      case TailExt(e) => normalizeType(typeOf(e,nv,tnv),tnv) match {
       case ListT(x) => ListT(x)
       case _ => throw TypeException("head not a list")
      }
      case LetType(x, t, e) => {
       val tnv2 = TVBind(x,normalizeType(t,tnv))::tnv
       normalizeType(typeOf(e,nv,tnv2),tnv2)
      }
    }
  }

  def lookup(x: String, nv: List[TBind]): Type = nv match {
    case Nil => throw TypeException("lookup: empty list")
    case TBind(str,t) :: tail => if(str == x) t else lookup(x, tail)
    case _ => throw TypeException("no tbind in nv")
  }


  def tlookup(x: String, tnv: List[TVBind]): Type = tnv match {
    case Nil => throw TypeException("tlookup: empty list")
    case TVBind(str,t) :: tail => if(str == x) normalizeType(t,tnv) else tlookup(x, tail)
    case _ => throw TypeException("no tvbind in tnv")
  }

  def normalizeType(t: Type, tnv: List[TVBind]): Type = t match {
    case VarT(a) => tlookup(a,tnv)
    case FunT(in, out) => FunT(normalizeType(in,tnv), normalizeType(out,tnv))
    case NumT() => NumT()
    case ListT(a) => ListT(normalizeType(a,tnv))
    case _ => {
      println("nt: " + t)
      throw TypeException("another thing than var?")
    }
  }


}

sealed abstract class ExprExt

case class NumExt(n: Int)                          extends ExprExt
case class PlusExt(e1: ExprExt, e2: ExprExt)       extends ExprExt
case class MultExt(e1: ExprExt, e2: ExprExt)       extends ExprExt
case class FdExt(x: String, t: Type, e: ExprExt)   extends ExprExt
case class AppExt(f: ExprExt, a: ExprExt)          extends ExprExt
case class IdExt(x: String)                        extends ExprExt
case class ConsExt(hd: ExprExt, tl: ExprExt)       extends ExprExt
case class NilExt(t: Type)                         extends ExprExt
case class HeadExt(e: ExprExt)                     extends ExprExt
case class TailExt(e: ExprExt)                     extends ExprExt
case class LetType(x: String, t: Type, e: ExprExt) extends ExprExt

sealed abstract class Type

case class NumT()                 extends Type
case class ListT(t: Type)         extends Type
case class FunT(a: Type, r: Type) extends Type
case class VarT(x: String)        extends Type

case class TBind(x: String, t: Type)

case class TVBind(x: String, t: Type)