#include <stdio.h>
#include <stdlib.h>

void Msg(char* msg) {
    printf(msg);    
}

/***************************************************************************/

typedef char* Ide;

Ide New(char* string) {
    return string;   
}

int Equal(Ide ide1, Ide ide2) {
    return strcmp(ide1, ide2) == 0;
}

/***************************************************************************/

typedef struct ExpBase* Exp;
typedef struct DeclBase* Decl;

typedef enum ExpClass {
    IdeClass = 1, CondClass, LambClass, ApplClass, BlockClass
} ExpClass;

typedef struct ExpBase {
    ExpClass class_;
    Ide ide;                    // IdeClass
    Exp test, ifTrue, ifFalse;  // CondClass
    Ide binder; Exp body;       // LambClass
    Exp fun, arg;               // ApplClass
    Decl decl; Exp scope;       // BlockClass
} ExpBase;

typedef enum DeclClass {
    DefClass = 1, SeqClass, RecClass   
} DeclClass;

typedef struct DeclBase {
    DeclClass class_;
    Ide binder; Exp def;        // DefClass
    Decl first, second;         // SeqClass
    Decl rec;                   // RecClass
} DeclBase;

Exp NewIdeExp(Ide ide) {
    Exp r = (Exp)malloc(sizeof(ExpBase));
    r->class_ = IdeClass; r->ide = ide;
    return r;
}

Exp NewCondExp(Exp test, Exp ifTrue, Exp ifFalse) {
    Exp r = (Exp)malloc(sizeof(ExpBase));
    r->class_ = CondClass; r->test = test; r->ifTrue = ifTrue; r->ifFalse = ifFalse;
    return r;
}

Exp NewLambExp(Ide binder, Exp body) {
    Exp r = (Exp)malloc(sizeof(ExpBase));
    r->class_ = LambClass; r->binder = binder; r->body = body;
    return r;
}

Exp NewApplExp(Exp fun, Exp arg) {
    Exp r = (Exp)malloc(sizeof(ExpBase));
    r->class_ = ApplClass; r->fun = fun; r->arg = arg;
    return r;
}

Exp NewBlockExp(Decl decl, Exp scope) {
    Exp r = (Exp)malloc(sizeof(ExpBase));
    r->class_ = BlockClass; r->decl = decl; r->scope = scope;
    return r;
}

Decl NewDefDecl(Ide binder, Exp def) {
    Decl r = (Decl)malloc(sizeof(DeclBase));
    r->class_ = DefClass; r->binder = binder; r->def = def;
    return r;
}

Decl NewSeqDecl(Decl first, Decl second) {
    Decl r = (Decl)malloc(sizeof(DeclBase));
    r->class_ = SeqClass; r->first = first; r->second = second;
    return r;
}

Decl NewRecDecl(Decl rec) {
    Decl r = (Decl)malloc(sizeof(DeclBase));
    r->class_ = RecClass; r->rec = rec;
    return r;
}


/***************************************************************************/

typedef struct TypeExpBase* TypeExp;

typedef enum TypeClass {
        VarType = 1, OperType
} TypeClass;

struct TypeListBase;
typedef struct TypeListBase* TypeList;

typedef struct TypeExpBase {
    TypeClass class_;
    TypeExp instance;           // VarType
    Ide ide; TypeList args;     // OperType
} TypeExpBase;

typedef struct TypeListBase {
    TypeExp head;
    TypeList tail;   
} TypeListBase;

TypeExp NewTypeVar() {
    TypeExp r = (TypeExp)malloc(sizeof(TypeExpBase));
    r->class_ = VarType; r->instance=NULL; return r;   
}

TypeExp NewTypeOper(Ide ide, TypeList args) {
    TypeExp r = (TypeExp)malloc(sizeof(TypeExpBase));
    r->class_ = OperType; r->ide = ide; r->args = args; return r;
}

TypeList Extend(TypeExp head, TypeList tail) {
    TypeList r = (TypeList)malloc(sizeof(TypeListBase));
    r->head = head; r->tail = tail; return r;  
}

int SameType(TypeExp typeExp1, TypeExp typeExp2) {
    return typeExp1 == typeExp2;
}

TypeExp Prune(TypeExp typeExp) {
    switch(typeExp->class_) {
        case VarType:
            if(typeExp->instance == NULL)
                return typeExp;
            else {
                typeExp->instance = Prune(typeExp->instance);
                return typeExp->instance;
            }
        case OperType:
            return typeExp;
    }   
}

int OccursInType(TypeExp typeVar, TypeExp typeExp) {
    typeExp = Prune(typeExp);
    switch(typeExp->class_) {
        case VarType:
            return SameType(typeVar, typeExp);
        case OperType:
            return OccursInTypeList(typeVar, typeExp->args);
    }
}

int OccursInTypeList(TypeExp typeVar, TypeList list) {
    if(list==NULL) return 0;
    if(OccursInType(typeVar, list->head)) return 1;
    return OccursInTypeList(typeVar, list->tail);
}

TypeList Empty;

void UnifyArgs(TypeList list1, TypeList list2);

void UnifyType(TypeExp typeExp1, TypeExp typeExp2) {
    typeExp1 = Prune(typeExp1);
    typeExp2 = Prune(typeExp2);
    switch(typeExp1->class_) {
        case VarType:
            if(OccursInType(typeExp1, typeExp2)) {
                if(!SameType(typeExp1, typeExp2))
                    Msg("Type clash");
            } else
                typeExp1->instance = typeExp2;
            break;
        case OperType:
            switch(typeExp2->class_) {
                case VarType:
                    UnifyType(typeExp2, typeExp1);
                    break;
                case OperType:
                    if(Equal(typeExp1->ide, typeExp2->ide))
                        UnifyArgs(typeExp1->args, typeExp2->args);
                    else
                        Msg("Type clash");
            }
    }
}

void UnifyArgs(TypeList list1, TypeList list2) {
    if(list1==Empty && list2==Empty) return;
    if(list1==Empty || list2==Empty)
        Msg("Type clash");
    else {
        UnifyType(list1->head, list2->head);
        UnifyArgs(list1->tail, list2->tail);
    }
}

/***************************************************************************/

typedef TypeList NonGenericVars;

NonGenericVars EmptyGen;

NonGenericVars ExtendGen(TypeExp head, NonGenericVars tail) {
    return Extend(head, tail);
}

int IsGeneric(TypeExp typeVar, NonGenericVars list) {
    return !OccursInTypeList(typeVar, list);
}

typedef struct CopyEnvBase* CopyEnv;

typedef struct CopyEnvBase {
    TypeExp old, new_;
    CopyEnv tail;
} CopyEnvBase;

CopyEnv ExtendCopyEnv(TypeExp old, TypeExp new_, CopyEnv tail) {
    CopyEnv r = (CopyEnv)malloc(sizeof(CopyEnvBase));
    r->old = old; r->new_ = new_; r->tail = tail; return r;
}

TypeExp FreshVar(TypeExp typeVar, CopyEnv scan, CopyEnv* env) {
    TypeExp newTypeVar;
    if(scan==NULL) {
        newTypeVar = NewTypeVar();
        *env = ExtendCopyEnv(typeVar, newTypeVar, *env);
        return newTypeVar;
    } else if(SameType(typeVar, scan->old))
        return scan->new_;
    else
        return FreshVar(typeVar, scan->tail, /*VAR*/ env);
}

TypeExp Fresh(TypeExp typeExp, NonGenericVars list, CopyEnv* env);

TypeList FreshList(TypeList args, NonGenericVars list, CopyEnv* env) {
    if(args==Empty) return Empty;
    return Extend(Fresh(args->head, list, /*VAR*/ env),
        FreshList(args->tail, list, /*VAR*/ env));
}

TypeExp Fresh(TypeExp typeExp, NonGenericVars list, CopyEnv* env) {
    typeExp = Prune(typeExp);
    switch(typeExp->class_) {
        case VarType:
            if(IsGeneric(typeExp, list))
                return FreshVar(typeExp, *env, /*VAR*/ env);
            else
                return typeExp;
        case OperType:
            return NewTypeOper(typeExp->ide, 
                FreshList(typeExp->args, list, /*VAR*/ env));
    }
}

TypeExp FreshType(TypeExp typeExp, NonGenericVars list) {
    CopyEnv env=NULL;
    return Fresh(typeExp, list, /*VAR*/ &env);
}

/***************************************************************************/

typedef struct EnvBase* Env;

Env EmptyEnv;

typedef struct EnvBase {
    Ide ide;
    TypeExp typeExp;
    Env tail;   
} EnvBase;

Env ExtendEnv(Ide ide, TypeExp typeExp, Env tail) {
    Env r = (Env)malloc(sizeof(EnvBase));
    r->ide = ide; r->typeExp = typeExp; r->tail = tail; return r;
}

TypeExp Retrieve(Ide ide, Env env, NonGenericVars list) {
    if(env==EmptyEnv) {
        printf("Unbound ide %s", ide);
        return NULL;
    } else if(Equal(ide, env->ide))
        return FreshType(env->typeExp, list);
    else
        return Retrieve(ide, env->tail, list);
}

/***************************************************************************/

TypeExp BoolType, MsgType;

TypeExp FunType(TypeExp dom, TypeExp cod) {
    return NewTypeOper(New("->"), Extend(dom, Extend(cod, Empty)));
}

Env AnalyzeDecl(Decl decl, Env env, NonGenericVars list);

TypeExp AnalyzeExp(Exp exp, Env env, NonGenericVars list) {
    TypeExp typeOfThen, typeOfElse, typeOfBinder, typeOfBody, 
            typeOfFun, typeOfArg, typeOfRes;
    Env bodyEnv, declEnv;
    NonGenericVars bodyList;
    switch(exp->class_) {
        case IdeClass:
            return Retrieve(exp->ide, env, list);
        case CondClass:
            UnifyType(AnalyzeExp(exp->test, env, list), BoolType);
            typeOfThen = AnalyzeExp(exp->ifTrue, env, list);
            typeOfElse = AnalyzeExp(exp->ifFalse, env, list);
            UnifyType(typeOfThen, typeOfElse);
            return typeOfThen;
        case LambClass:
            typeOfBinder = NewTypeVar();
            bodyEnv = ExtendEnv(exp->binder, typeOfBinder, env);
            bodyList = ExtendGen(typeOfBinder, list);
            typeOfBody = AnalyzeExp(exp->body, bodyEnv, bodyList);
            return FunType(typeOfBinder, typeOfBody);
        case ApplClass:
            typeOfFun = AnalyzeExp(exp->fun, env, list);
            typeOfArg = AnalyzeExp(exp->arg, env, list);
            typeOfRes = NewTypeVar();
            UnifyType(typeOfFun, FunType(typeOfArg, typeOfRes));
            return typeOfRes;
        case BlockClass:
            declEnv = AnalyzeDecl(exp->decl, env, list);
            return  AnalyzeExp(exp->scope, declEnv, list);
    }
}

void AnalyzeRecDeclBind(Decl decl, Env* env, NonGenericVars* list);
void AnalyzeRecDecl(Decl decl, Env env, NonGenericVars list);

Env AnalyzeDecl(Decl decl, Env env, NonGenericVars list) {
    TypeExp newTypeVar;
    switch(decl->class_) {
        case DefClass:
            return ExtendEnv(decl->binder, 
                AnalyzeExp(decl->def, env, list), env);
        case SeqClass:
            return AnalyzeDecl(decl->second, 
                AnalyzeDecl(decl->first, env, list), list);
        case RecClass:
            AnalyzeRecDeclBind(decl->rec, /*VAR*/ &env, /*VAR*/ &list);
            AnalyzeRecDecl(decl->rec, env, list);
            return env;
    }
}

void AnalyzeRecDeclBind(Decl decl, Env* env, NonGenericVars* list) {
    TypeExp newTypeVar;
    switch(decl->class_) {
        case DefClass:
            newTypeVar = NewTypeVar();
            *env = ExtendEnv(decl->binder, newTypeVar, *env);
            *list = ExtendGen(newTypeVar, *list);
            break;
        case SeqClass:
            AnalyzeRecDeclBind(decl->first, /*VAR*/ env, /*VAR*/ list);
            AnalyzeRecDeclBind(decl->second, /*VAR*/ env, /*VAR*/ list);
            break;
        case RecClass:
            AnalyzeRecDeclBind(decl->rec, /*VAR*/ env, /*VAR*/ list);
    }
}

void AnalyzeRecDecl(Decl decl, Env env, NonGenericVars list) {
    switch(decl->class_) {
        case DefClass:
            UnifyType(Retrieve(decl->binder, env, list), 
                AnalyzeExp(decl->def, env, list));
            break;
        case SeqClass:
            AnalyzeRecDecl(decl->first, env, list);
            AnalyzeRecDecl(decl->second, env, list);
            break;
        case RecClass:
            AnalyzeRecDecl(decl->rec, env, list);
   }
}

/***************************************************************************/

int main(int argc, char *argv[])
{

  Empty=NULL;
  EmptyGen=Empty;
  EmptyEnv=NULL;
  BoolType = NewTypeOper(New("bool"), Empty);
  MsgType = NewTypeOper(New("msg"), Empty);

  Env env = ExtendEnv(New("bool"), BoolType, EmptyEnv);
  env = ExtendEnv(New("msg"), MsgType, env);

  Ide x = New("x");
  Exp id = NewLambExp(x, NewIdeExp(x));

  Decl a = NewDefDecl(New("a"), id);
  Decl b = NewDefDecl(New("b"), NewApplExp(NewIdeExp("a"), NewIdeExp(New("bool"))));
  Decl c = NewDefDecl(New("c"), NewApplExp(NewIdeExp("a"), NewIdeExp(New("msg"))));

  Exp test = NewBlockExp(NewRecDecl(NewSeqDecl(a, NewSeqDecl(b, c))), NewIdeExp("a"));

  TypeExp typ = AnalyzeExp(test, env, EmptyGen);

  printf("%s\n", typ->ide);

  TypeList j = typ->args;
  while(j) {
      printf("arg: %d\n", j->head->class_);
      j = j->tail;
  }

  /*
  Ide y = New("bool");
  Exp appl = NewApplExp(id, NewIdeExp(y));

  Decl dec1 = NewDefDecl(New("id"), id);
  Decl dec2 = NewDefDecl(New("appl"), appl);

  Decl dec = NewRecDecl(NewSeqDecl(dec1, dec2));

  Env env = ExtendEnv(y, BoolType, EmptyEnv);

  //env = AnalyzeDecl(dec, env, EmptyGen);

  env = AnalyzeDecl(dec2, AnalyzeDecl(dec1, env, EmptyGen), EmptyGen);
   */
/*
  Env i = env;
  while(i) { 
    printf("ident: %s\n", i->ide);
   
    TypeExp typeExp = i->typeExp;

    printf("typeExp: %d\n", typeExp->class_);
    if(typeExp->class_==2) {
        TypeList j = typeExp->args;
        while(j) {
            printf("arg: %d\n", j->head->class_);
            j = j->tail;
        }
    }
    //if(i->typeExp->class_==1 && i->typeExp->instance!=NULL)
    //    printf("typeExp: %d\n", i->typeExp->instance->class_);
    //else
    //    printf("typeExp: %d\n", i->typeExp->class_);
    i = i->tail; 
  }
*/
 /*
  Ide x = New("x");
  Ide y = New("y");
  Ide z = New("z");

  Env env = ExtendEnv(z, BoolType, EmptyEnv);
  env = ExtendEnv(y, BoolType, env);

  Exp id = NewLambExp(x, NewIdeExp(x));

  //TypeExp res = AnalyzeExp(NewApplExp(id, NewIdeExp(y)), env, EmptyGen);
  
  TypeExp res = AnalyzeExp(id, env, EmptyGen);

  printf("class: %s\n", res->ide);
  if(res->args->head==res->args->tail->head) printf("hallo");
*/

  //printf("class: %s\n", (int)res->instance->ide);
  getch();

  return 0;
}