aspect TypeAnalysis {
  
  // ***API***
  
  // Declaration of *type*
  // Refers to the appropriate type of the declaration or expression,
  // or refers to unknownDecl if there is no appropriate type in the program.
  syn lazy TypeDecl Decl.type();
  syn lazy TypeDecl Exp.type();

  // Declaration of *isSubtypeOf*
  // Compares two types
  syn lazy boolean TypeDecl.isSubtypeOf(TypeDecl typeDecl);

  // Declaration of *isValue*
  // True if the expression denotes a value, i.e., something that can be assigned to a variable.
  syn boolean Exp.isValue();

  // *hasCycleOnSuperclassChain* - true if there is a cycle somewhere on the superclass chain
  // Defined using a circular attribute.
  syn lazy boolean ClassDecl.hasCycleOnSuperclassChain() circular [true];
  
  // *superClass* - the superclass declaration
  // - if it exists and if there are no cycles on the superclass chain
  // - otherwise null
  syn lazy ClassDecl ClassDecl.superClass();
  
  
  // ***Implementation***
  
  // Definition of *type*
  eq TypeDecl.type() = this;
  eq VarDecl.type() = getType().decl().type();

  eq IdUse.type() = decl().type();
  eq Dot.type() = getIdUse().type();

  eq BooleanLiteral.type() = booleanType();

  // Definition of *isSubtypeOf*
  // use double dispatch to allow modular extension of type comparisons
  eq TypeDecl.isSubtypeOf(TypeDecl typeDecl) = typeDecl.isSuperTypeOf(this);
  eq ClassDecl.isSubtypeOf(TypeDecl typeDecl) = typeDecl.isSuperTypeOfClassDecl(this);

  syn lazy boolean TypeDecl.isSuperTypeOf(TypeDecl typeDecl) = this == typeDecl;
  syn lazy boolean TypeDecl.isSuperTypeOfClassDecl(ClassDecl typeDecl) = 
    this == typeDecl || typeDecl.superClass() != null && typeDecl.superClass().isSubtypeOf(this);
    
  // Definition of *superClass*
  eq ClassDecl.superClass() {
    if (hasSuperclass() && getSuperclass().decl() instanceof ClassDecl && !hasCycleOnSuperclassChain())
      return (ClassDecl) getSuperclass().decl();
    else
      return null;
  }

  // *hasCycleOnSuperclassChain* - true if there is a cycle somewhere on the superclass chain
  eq ClassDecl.hasCycleOnSuperclassChain() {
    if (hasSuperclass() && getSuperclass().decl() instanceof ClassDecl) //First, check if there is a superclass
      return ((ClassDecl) getSuperclass().decl()).hasCycleOnSuperclassChain();
    else
      return false;
  }

  // Definition of *isValue*
  eq Exp.isValue() = true;
  eq Dot.isValue() = getIdUse().isValue();

  eq TypeUse.isValue() = false;
  // Note! If we did not have the rewrites below, the above equation would have to instead be written as:
  // eq IdUse.isValue() = !(decl() instanceof TypeDecl)

  // Rewrite rules for replacing Use-nodes based on their declaration kind
  rewrite Use {
    when(decl() instanceof VarDecl)
    to VariableUse new VariableUse(getName());
  }
  
  rewrite Use {
    when(decl() instanceof TypeDecl)
    to TypeUse new TypeUse(getName());
  }
}