#include "fullfomsubref.h"

Ty* maketop(Kind* kn) {
    Ty* result_ty;
    switch(kn->_kn_name){
        case KnStar:
            result_ty = new Ty(TyTop);
            break;
        case KnArr:
            result_ty = new Ty(TyAbs, "_", kn->_kn0, maketop(kn->_kn1));
            break;
    }
    return result_ty;
}


Ty* promote(Ty* ty) {
    Ty* result_ty, *ty0;
    Binding* b;
    switch(ty->_typ) {
        case TyVar:
            b = getbinding(ty->_db_index);
            if (b->_binding_name == TyVarBind)
                result_ty = b->_ty;
            else{
                result_ty = new Ty(TYNoRuleApplies);
            }
            break;
        case TyApp:
            result_ty = new Ty(TyApp, promote(ty->_ty0), ty->_ty1);            
            break;
        default:
            result_ty = new Ty(TYNoRuleApplies);
            break;
    }
    return result_ty;
}


Ty* lcst(Ty* ty) {
    Ty *result_ty, *ty0, *ty1; 
    ty0 = simplifyty(ty);
    ty1 = promote(ty0);
    if (ty1->_typ == TYNoRuleApplies)
        return ty0;
    ty1 = lcst(ty1);
    if (ty1->_typ == TYNoRuleApplies)
        return ty0;
    else       
        return ty1;
}


string proty(Ty* ty) {
    if (ty->_typ != TyTop)
        return "<:" + ty->getTy_str();
    else
        return "";
}


string Ty::getTy_str() {
    string result_str, uv_str, kn_str, proty_str;
    switch (_typ) {
        case TyUnit:
            result_str = "Unit";
            break;
        case TyString:
            result_str = "String";
            break;
        case TyBool:
            result_str = "Bool";
            break;
        case TyNat:
            result_str = "Nat";
            break;
        case TyFloat:
            result_str = "Float";
            break;
        case TyTop:
            result_str = "Top";
            break;
        case TyBot:
            result_str = "Bot";
            break;
        case TyArr:
            result_str = "(" + _ty0->getTy_str() + " -> " + _ty1->getTy_str() + ")";
            break;
        case TyRecord:
            result_str = "{";
            for (int i = 0; i < _ftys->size(); i++){
                if(_ftys->at(i)->_label == to_string(i + 1))
                    result_str += _ftys->at(i)->_ty->getTy_str();
                else
                    result_str +=  _ftys->at(i)->_label + ":" + _ftys->at(i)->_ty->getTy_str();
                if ((i + 1) != _ftys->size())
                    result_str += ", ";
            }
            result_str += "}";
            break;
        case TyVariant:
            result_str = "<";
            for (int i = 0; i < _ftys->size(); i++){
                if(_ftys->at(i)->_label == to_string(i + 1))
                    result_str += _ftys->at(i)->_ty->getTy_str();
                else
                    result_str +=  _ftys->at(i)->_label + ":" + _ftys->at(i)->_ty->getTy_str();
                if ((i + 1) != _ftys->size())
                    result_str += ", ";
            }
            result_str += ">";
            break;
        case TyVar:
            result_str = index2name(_db_index);
            break;
        case TyId:
            result_str = _u_var_str;
            break;
        case TyError:
            result_str = "Type Error";
            break;
        case TySome:
            proty_str = proty(_ty0);
            uv_str = pickfreshname(_u_var_str);
            result_str = "{Some " + uv_str + " " + proty_str + "," + _ty1->getTy_str() + "}";
            _context.pop_back();
            break;      
        case TyAll:
            proty_str = proty(_ty0);
            uv_str = pickfreshname(_u_var_str);
            result_str = "All " + uv_str + " " + proty_str + "." + _ty1->getTy_str();
            _context.pop_back();
            break;   
        case TyAbs:
            kn_str =_kn0->getKind_str();
            uv_str = pickfreshname(_u_var_str);
            result_str = "(lambda " + uv_str +"::"+ kn_str + "." + _ty0->getTy_str() + ")";
            _context.pop_back();
            break;
        case TyApp:
            result_str = "(" + _ty0->getTy_str() + " " + _ty1->getTy_str() + ")";
            break;
        case TyRef:
            result_str = "Ref " +  _ty0->getTy_str();
            break;
        case TySource:
            result_str = "Source " +  _ty0->getTy_str();
            break;
        case TySink:
            result_str = "Sink " +  _ty0->getTy_str();
            break;
        case TyNone:
            result_str = "TyNone";
            break;    
        case TYNoRuleApplies:
            result_str = "TYNoRuleApplies";
            break;               
    }
    return result_str;
}      


string Kind::getKind_str() {
    string result_str;
    switch (_kn_name){
        case KnStar:
            result_str = "*";
            break;
        case KnArr:
            result_str = "(" + _kn0->getKind_str() + " => " + _kn1->getKind_str() + ")";
            break;
        case KnNone:
            result_str = "";
            break;
    }
    return result_str;
}


Ty* copyTy(Ty* ty){
    Ty* result_ty;
    FieldTys* ftys;
    switch (ty->_typ) {
        case TyUnit:
        case TyBool:
        case TyNat:
        case TyFloat:
        case TyNone:
        case TyString:
        case TyBot:
        case TyTop:
        case TyError:
        case TYNoRuleApplies:
        case TyNotFound:
            result_ty = new Ty(ty->_typ);
            break;
        case TyArr:
        case TyApp:
            result_ty = new Ty(ty->_typ, copyTy(ty->_ty0), copyTy(ty->_ty1));
            break;
        case TyRecord:
        case TyVariant:
            ftys = new FieldTys();
            for (int i = 0; i < ty->_ftys->size(); i++)
                ftys->push_back(copyFieldTy(ty->_ftys->at(i)));
            result_ty  = new Ty(ty->_typ, ftys);
            break;
        case TyVar:
            result_ty = new Ty(TyVar, ty->_db_index);
            break;
        case TyId:
            result_ty = new Ty(TyId, ty->_u_var_str);
            break;
        case TyAbs:
            result_ty = new Ty(TyAbs, ty->_u_var_str, copyKind(ty->_kn0), copyTy(ty->_ty0));
            break;
        case TyAll:
        case TySome:
            result_ty = new Ty(ty->_typ, ty->_u_var_str, copyTy(ty->_ty0), copyTy(ty->_ty1));
            break;
        case TyRef:
        case TySource:
        case TySink:
            result_ty = new Ty(ty->_typ, copyTy(ty->_ty0));
            break;
    }
    return result_ty;
}


FieldTy* copyFieldTy(FieldTy* fty) { return new FieldTy(fty->_label, copyTy(fty->_ty));}


Kind* copyKind(Kind* kn);

Kind* copyKind(Kind* kn){
    Kind* result_kn;
    switch (kn->_kn_name) {
        case KnStar:
        case KnNone:
            result_kn = new Kind(kn->_kn_name);
            break;
        case KnArr:
            result_kn = new Kind(KnArr, copyKind(kn->_kn0), copyKind(kn->_kn1));
            break;
    }
    return result_kn;
}


Ty* typeShiftAbove(int d, int c, Ty* ty) {
    Ty* result_ty;
    FieldTys* ftys;
    FieldTy* fty;
    Ty* ty0;
    int i;
    switch (ty->_typ){
        case TyArr:
        case TyApp:
            result_ty = new Ty(ty->_typ, typeShiftAbove(d, c, ty->_ty0),  typeShiftAbove(d, c, ty->_ty1));
            break;
        case TyUnit:
        case TyBool:
        case TyNat:
        case TyString:
        case TyFloat:
        case TyBot:
        case TyTop:
            result_ty = new Ty(ty->_typ);           
            break;
        case TyVar:
            if (ty->_db_index >= c)
                result_ty = new Ty(TyVar, ty->_db_index + d);
            else
                result_ty = new Ty(TyVar, ty->_db_index);
            break;
        case TyRecord:
        case TyVariant:
            ftys = new FieldTys();
            for (i = 0; i < ty->_ftys->size(); i++){
                ty0 = typeShiftAbove(d, c, ty->_ftys->at(i)->_ty);
                ftys->push_back(new FieldTy(ty->_ftys->at(i)->_label, ty0));
            }
            result_ty  = new Ty(ty->_typ, ftys);
            break;
        case TyId:
            result_ty = new Ty(TyId, ty->_u_var_str);
            break;
       case TyAbs:
            result_ty = new Ty(TyAbs, ty->_u_var_str, ty->_kn0, typeShiftAbove(d, c + 1, ty->_ty0));
            break;
        case TySome:
        case TyAll:
            result_ty = new Ty(ty->_typ, ty->_u_var_str, typeShiftAbove(d, c, ty->_ty0), typeShiftAbove(d, c + 1, ty->_ty1));
            break;
        case TyRef:
        case TySource:
        case TySink:
            result_ty = new Ty(ty->_typ, typeShiftAbove(d, c, ty->_ty0));
            break;
    }
    return result_ty;
}


Ty* typeShift(int d, Ty* ty){ return typeShiftAbove(d, 0, ty);}


Ty* typeSubst(Ty* tyS, int j, Ty* tyT) {
    Ty* result_ty;
    FieldTys* ftys;
    FieldTy* fty;
    Ty* ty0;
    int i;
    Binding* bind;
    switch (tyT->_typ){
        case TyArr:
        case TyApp:
            result_ty = new Ty(tyT->_typ, typeSubst(tyS, j, tyT->_ty0), typeSubst(tyS, j, tyT->_ty1));
            break;
        case TyUnit:
        case TyBool:
        case TyNat:
        case TyString:
        case TyFloat:
        case TyBot:
        case TyTop:
            result_ty = new Ty(tyT->_typ);           
            break;
        case TyVar:
            if (tyT->_db_index == j)
                result_ty = typeShift(j, tyS);
            else
                result_ty = new Ty(TyVar, tyT->_db_index);
            break;
        case TyRecord:
        case TyVariant:
            ftys = new FieldTys();
            for (i = 0; i < tyT->_ftys->size(); i++){
                ty0 = typeSubst(tyS, j, tyT->_ftys->at(i)->_ty);
                ftys->push_back(new FieldTy(tyT->_ftys->at(i)->_label, ty0));
            }
            result_ty  = new Ty(tyT->_typ, ftys);
            break;
        case TyId:
            result_ty = new Ty(TyId, tyT->_u_var_str);
            break;
        case TyAbs:
            result_ty = new Ty(tyT->_typ, tyT->_u_var_str, tyT->_kn0, typeSubst(tyS, j + 1, tyT->_ty0));
            break;
        case TySome:
        case TyAll:
            result_ty = new Ty(tyT->_typ, tyT->_u_var_str, typeSubst(tyS, j, tyT->_ty0), typeSubst(tyS, j + 1, tyT->_ty1));
            break;
        case TyRef:
        case TySource:
        case TySink:
            result_ty = new Ty(tyT->_typ, typeSubst(tyS, j, tyT->_ty0));
            break;
    }
    return result_ty;
}


Ty* typeSubstTop(Ty* tyS, Ty* tyT){ return typeShift(-1, typeSubst(typeShift(1, tyS), 0, tyT));}


Binding* evalbinding(Binding* b){
    Binding* result_bind;
    bool NoRuleApplies0 = false;
    bool ErrorEncountered0 = false;
    if (b->_binding_name == TmAbbBind){
        b->_term = eval(b->_term, &NoRuleApplies0, &ErrorEncountered0);
        result_bind = b;
    }
    else
        result_bind = b;
     return result_bind;
}


bool istyabb(int i){
    bool result_b;
    Binding* b = getbinding(i);
    if (b->_binding_name == TyAbbBind)
        result_b = true;
    else
        result_b = false;
    return result_b;
} 

  
Ty* gettyabb(int i){
    Ty* result_ty;
    Binding* b = getbinding(i);
    if (b->_binding_name == TyAbbBind)
        result_ty = b->_ty;
    else
        result_ty = new Ty(TYNoRuleApplies);
    return result_ty;
}


Ty* computety(Ty* ty){
    Ty* result_ty;
    if (ty->_typ == TyVar && istyabb(ty->_db_index))
        result_ty = gettyabb(ty->_db_index);
    else if (ty->_typ == TyApp && ty->_ty0->_typ == TyAbs)
        result_ty = typeSubstTop(ty->_ty1, ty->_ty0->_ty0);
    else {
        result_ty = new Ty(TYNoRuleApplies);
    }
    return result_ty;
}


Ty* simplifyty(Ty* ty) {
    //if (ty->_typ == TYNoRuleApplies) return ty;
    Ty *ty0, *ty1, *ty2;
    if (ty->_typ == TyApp)
        ty0 = new Ty(TyApp, simplifyty(ty->_ty0), ty->_ty1);
    else
        ty0 = ty;
    ty1 = computety(ty0);
    if (ty1->_typ == TYNoRuleApplies)
        return ty0;
    else{
        ty2 = simplifyty(ty1);
        if (ty2->_typ == TYNoRuleApplies)
            return ty0;
        else
            return ty2;
    }
}


bool tyeqv (Ty* ty0, Ty* ty1) {
    bool result_b;
    int i, j;
    Binding *bind;
    Ty* tyS = simplifyty(ty0);
    Ty* tyT = simplifyty(ty1);
    if (tyS->_typ == TyArr && tyT->_typ == TyArr)
        result_b = tyeqv (tyS->_ty0, tyT->_ty0) && tyeqv (tyS->_ty1, tyT->_ty1);
    else if (tyS->_typ == TyTop && tyT->_typ == TyTop)
        result_b = true;
    else if (tyS->_typ == TyId && tyT->_typ == TyId)
        result_b = (tyS->_u_var_str == tyT->_u_var_str);
    else if (tyS->_typ == TyString && tyT->_typ == TyString)
        result_b = true;
    else if (tyS->_typ == TyUnit && tyT->_typ == TyUnit)
        result_b = true;    
    else if (tyS->_typ == TyFloat && tyT->_typ == TyFloat)
        result_b = true;
    else if (tyS->_typ == TyVar && istyabb(tyS->_db_index))
        result_b = tyeqv(gettyabb(tyS->_db_index), tyT);
    else if (tyT->_typ == TyVar && istyabb(tyT->_db_index))
        result_b = tyeqv(tyS, gettyabb(tyT->_db_index));
    else if (tyS->_typ == TyVar && tyT->_typ == TyVar)
        result_b = (tyS->_db_index == tyT->_db_index);    
    else if (tyS->_typ == TyBool && tyT->_typ == TyBool)
        result_b = true;
    else if (tyS->_typ == TyNat && tyT->_typ == TyNat)
        result_b = true;   
    else if ((tyS->_typ == TyRecord && tyT->_typ == TyRecord) || (tyS->_typ == TyVariant && tyT->_typ == TyVariant)){
        result_b = (tyS->_ftys->size() == tyT->_ftys->size());
        if (result_b) {
            for (i = 0; i < tyT->_ftys->size(); i++){                 
                for (j = 0; j < tyS->_ftys->size(); j++){
                    if (tyT->_ftys->at(i)->_label == tyS->_ftys->at(j)->_label){
                        result_b = tyeqv(tyS->_ftys->at(j)->_ty, tyT->_ftys->at(i)->_ty);
                        break;
                    }
                      
                } 
                if ((j >= tyS->_ftys->size()) || !result_b){
                    result_b = false;
                    break;
                }                      
            }   
        }            
    }
    else if (tyS->_typ == TySome && tyT->_typ == TySome){
        bind = new Binding(NameBind);
        _context.push_back(pair_sb(tyS->_u_var_str, bind));
        result_b = tyeqv(tyS->_ty0, tyT->_ty0) && tyeqv(tyS->_ty1, tyT->_ty1);
        _context.pop_back();   
    }
    else if (tyS->_typ == TyAll && tyT->_typ == TyAll){
        bind = new Binding(NameBind);
        _context.push_back(pair_sb(tyS->_u_var_str, bind));
        result_b = tyeqv(tyS->_ty0, tyT->_ty0) && tyeqv(tyS->_ty1, tyT->_ty1);
        _context.pop_back();   
    }
    else if (tyS->_typ == TyAbs && tyT->_typ == TyAbs){
        result_b = (tyS->_kn0->getKind_str() == tyT->_kn0->getKind_str());
        if (result_b) {
            bind = new Binding(NameBind);
            _context.push_back(pair_sb(tyS->_u_var_str, bind));
            result_b = tyeqv(tyS->_ty0, tyT->_ty0);
            _context.pop_back();
        }           
    }
    else if (tyS->_typ == TyApp && tyT->_typ == TyApp)
        result_b = tyeqv (tyS->_ty0, tyT->_ty0) && tyeqv (tyS->_ty1, tyT->_ty1);    
    else if (tyS->_typ == TyRef && tyT->_typ == TyRef)
        result_b = tyeqv(tyS->_ty0, tyT->_ty0);
    else if (tyS->_typ == TySource && tyT->_typ == TySource)
        result_b = tyeqv(tyS->_ty0, tyT->_ty0);
    else if (tyS->_typ == TySink && tyT->_typ == TySink)
        result_b = tyeqv(tyS->_ty0, tyT->_ty0);
    else
        result_b = false;
    return result_b;
}


bool subtype (Ty* ty0, Ty* ty1) {
    bool result_b = false;
    int i, j;
    Binding *bind;
    if (tyeqv(ty0, ty1))
        result_b = true;
    else {        
        Ty* tyS = simplifyty(ty0);
        Ty* tyT = simplifyty(ty1);
        if (tyT->_typ == TyTop)
            result_b = true;
        else if (tyS->_typ == TyBot)
            result_b = true;
        else if (tyS->_typ == TyArr && tyT->_typ == TyArr)
            result_b = subtype (tyT->_ty0, tyS->_ty0) && subtype (tyS->_ty1, tyT->_ty1);
        else if (tyS->_typ == TyRecord && tyT->_typ == TyRecord){
            for (i = 0; i < tyT->_ftys->size(); i++){                
                for (j = 0; j < tyS->_ftys->size(); j++){
                    if (tyT->_ftys->at(i)->_label == tyS->_ftys->at(j)->_label){
                        result_b = subtype(tyS->_ftys->at(j)->_ty, tyT->_ftys->at(i)->_ty);
                        break;
                    }
                }
                if ((j >= tyS->_ftys->size()) || !result_b){
                    result_b = false;
                    break;
                }
            }
        }
        else if (tyS->_typ == TyVariant && tyT->_typ == TyVariant){
            for (i = 0; i < tyS->_ftys->size(); i++){                
                for (j = 0; j < tyT->_ftys->size(); j++){
                    if (tyS->_ftys->at(i)->_label == tyT->_ftys->at(j)->_label){
                        result_b = subtype(tyS->_ftys->at(i)->_ty, tyT->_ftys->at(j)->_ty);
                        break;
                    }
                }
                if ((j >= tyT->_ftys->size()) || !result_b){
                    result_b = false;
                    break;
                }
            }
        }
        else if (tyS->_typ == TyVar)
            result_b = subtype(promote(tyS), tyT);
        else if ((tyS->_typ == TyAll && tyT->_typ == TyAll) || (tyS->_typ == TySome && tyT->_typ == TySome)){
            result_b = subtype (tyS->_ty0, tyT->_ty0) && subtype (tyT->_ty0, tyS->_ty0);
            if (result_b){
                bind = new Binding(TyVarBind, tyT->_ty0);
                _context.push_back(pair_sb(tyS->_u_var_str, bind));
                result_b = subtype(tyS->_ty1, tyT->_ty1);
                _context.pop_back(); 
            }              
        }
        else if (tyS->_typ == TyAbs && tyT->_typ == TyAbs){
            result_b = (tyS->_kn0->getKind_str() == tyT->_kn0->getKind_str());
            if (result_b){
                bind = new Binding(TyVarBind, maketop(tyS->_kn0));
                _context.push_back(pair_sb(tyS->_u_var_str, bind));
                result_b = subtype(tyS->_ty0, tyT->_ty0);
                _context.pop_back();
            }            
        }
        else if (tyS->_typ == TyApp)
            result_b = subtype(promote(tyS), tyT);
        else if (tyS->_typ == TyRef && tyT->_typ == TyRef)
            result_b = subtype (tyS->_ty0, tyT->_ty0) && subtype (tyT->_ty0, tyS->_ty0);
        else if (tyS->_typ == TyRef && tyT->_typ == TySource)
            result_b = subtype (tyS->_ty0, tyT->_ty0);
        else if (tyS->_typ == TySource && tyT->_typ == TySource)
            result_b = subtype (tyS->_ty0, tyT->_ty0);
        else if (tyS->_typ == TyRef && tyT->_typ == TySink)
            result_b = subtype (tyT->_ty0, tyS->_ty0);
        else if (tyS->_typ == TySink && tyT->_typ == TySink)
            result_b = subtype (tyT->_ty0, tyS->_ty0);              
        else
            result_b = false;
    } 
    return result_b;
}


vector<string>* getLabels (vector<FieldTy*>* ftys) {
    vector<string>* result_vs = new vector<string>;
    for (int i = 0; i < ftys->size(); i++)
        result_vs->push_back(ftys->at(i)->_label);
    sort(result_vs->begin(), result_vs->end());
    return result_vs;
}


Ty* meet (Ty* ty0, Ty* ty1);

Ty* join (Ty* ty0, Ty* ty1) {
    int i, j, k;
    Ty *result_ty, *meet_ty;
    Binding *bind;
    if (subtype(ty0, ty1)){
        result_ty = ty1;
    }        
    else if (subtype(ty1, ty0)){
        result_ty = ty0;
    }       
    else {
        Ty* tyS = simplifyty(ty0);
        Ty* tyT = simplifyty(ty1);
        if (tyS->_typ == TyRecord && tyT->_typ == TyRecord){
            vector<string>* labelsS;
            labelsS = getLabels(tyS->_ftys);
            vector<string>* labelsT;
            labelsT = getLabels(tyT->_ftys);
            vector<string>* commonLabels = new vector<string>;
            set_intersection(labelsS->begin(), labelsS->end(), labelsT->begin(), labelsT->end(), inserter(*commonLabels, commonLabels->end()));
            FieldTys* commonFields = new FieldTys;
            Ty *tySi, *tyTi;
            for (i = 0; i < commonLabels->size(); i++) {
                for (j = 0; j < tyS->_ftys->size(); j++) 
                    if (commonLabels->at(i) == tyS->_ftys->at(j)->_label){
                        tySi = tyS->_ftys->at(j)->_ty;
                        break;
                    }
                for (k = 0; k < tyT->_ftys->size(); k++) 
                    if (commonLabels->at(i) == tyT->_ftys->at(k)->_label){
                        tyTi = tyT->_ftys->at(k)->_ty;                        
                        break;
                    }
                if ((j < tyS->_ftys->size()) && (k < tyT->_ftys->size())){
                    commonFields->push_back(new FieldTy(commonLabels->at(i), join(tySi, tyTi)));
                }
            }
            result_ty = new Ty(TyRecord, commonFields);
        }
        else if (tyS->_typ == TyAll && tyT->_typ == TyAll){
            if (!(subtype (tyS->_ty0, tyT->_ty0) && subtype (tyT->_ty0, tyS->_ty0)))
                result_ty = new Ty(TyTop);
            else {
                bind = new Binding(TyVarBind, tyT->_ty0);
                _context.push_back(pair_sb(tyS->_u_var_str, bind));
                result_ty =  new Ty(TyAll, tyS->_u_var_str, tyS->_ty0, join(tyS->_ty1, tyT->_ty1));
                _context.pop_back(); 
            }              
        }
        else if (tyS->_typ == TyArr && tyT->_typ == TyArr)
            result_ty  = new Ty(TyArr, meet(tyS->_ty0, tyT->_ty0), join(tyS->_ty1, tyT->_ty1));
        else if(tyS->_typ == TyRef && tyT->_typ == TyRef) {
            if (!(subtype (tyS->_ty0, tyT->_ty0) && subtype (tyT->_ty0, tyS->_ty0)))
                result_ty = new Ty(TyRef, tyS->_ty0);
            else // Warning: this is incomplete... 
                 result_ty = new Ty(TySource, join(tyS->_ty0, tyT->_ty0));
        }        
        else if (tyS->_typ == TySource && tyT->_typ == TySource)
            result_ty = new Ty(TySource, join(tyS->_ty0, tyT->_ty0));
        else if (tyS->_typ == TyRef && tyT->_typ == TySource)
            result_ty = new Ty(TySource, join(tyS->_ty0, tyT->_ty0));
        else if (tyS->_typ == TySource && tyT->_typ == TyRef)
            result_ty = new Ty(TySource, join(tyS->_ty0, tyT->_ty0));
        else if (tyS->_typ == TySink && tyT->_typ == TySink)
            result_ty = new Ty(TySink, meet(tyS->_ty0, tyT->_ty0));
        else if (tyS->_typ == TyRef && tyT->_typ == TySink)
            result_ty = new Ty(TySink, meet(tyS->_ty0, tyT->_ty0));
        else if (tyS->_typ == TySink && tyT->_typ == TyRef)
            result_ty = new Ty(TySink, meet(tyS->_ty0, tyT->_ty0));               
        else
            result_ty  = new Ty(TyTop);
    }
    return result_ty;
}


Ty* meet (Ty* ty0, Ty* ty1) {
    Ty* result_ty;
    int i, j, k;
    Binding *bind;
    if (subtype(ty0, ty1))
         result_ty = ty0;
    else if (subtype(ty1, ty0))
         result_ty = ty1;
    else {
        Ty* tyS = simplifyty(ty0);
        Ty* tyT = simplifyty(ty1);
        if (tyS->_typ == TyRecord && tyT->_typ == TyRecord){
            vector<string>* labelsS;
            labelsS = getLabels(tyS->_ftys);
            vector<string>* labelsT;
            labelsT = getLabels(tyT->_ftys);
            vector<string>* allLabels = new vector<string>;;
            set_union(labelsS->begin(), labelsS->end(), labelsT->begin(), labelsT->end(), inserter(*allLabels, allLabels->end()));
            FieldTys* allFields = new FieldTys;
            Ty *tySi, *tyTi, *jointy;
            for (i = 0; i < allLabels->size(); i++) {
                for (j = 0; j < tyS->_ftys->size(); j++) 
                    if (allLabels->at(i) == tyS->_ftys->at(j)->_label){
                        tySi = tyS->_ftys->at(j)->_ty;
                        break;
                    }
                for (k = 0; k < tyT->_ftys->size(); k++) 
                    if (allLabels->at(i) == tyT->_ftys->at(k)->_label){
                        tyTi = tyT->_ftys->at(k)->_ty;
                        break;
                    }
                allFields->push_back(new FieldTy(allLabels->at(i), meet(tySi, tyTi)));
            }
            result_ty = new Ty(TyRecord, allFields);  
        }
        else if (tyS->_typ == TyAll && tyT->_typ == TyAll){
            if (!(subtype (tyS->_ty0, tyT->_ty0) && subtype (tyT->_ty0, tyS->_ty0)))
                result_ty = new Ty(TyNotFound);
            else {
                bind = new Binding(TyVarBind, tyT->_ty0);
                _context.push_back(pair_sb(tyS->_u_var_str, bind));
                result_ty =  new Ty(TyAll, tyS->_u_var_str, tyS->_ty0, meet(tyT->_ty0, tyT->_ty1));
                _context.pop_back(); 
            }              
        }
        else if (tyS->_typ == TyArr && tyT->_typ == TyArr)
            result_ty  = new Ty(TyArr, join(tyS->_ty0, tyT->_ty0), meet(tyS->_ty1, tyT->_ty1));
        else if(tyS->_typ == TyRef && tyT->_typ == TyRef) {
            if ((subtype (tyS->_ty0, tyT->_ty0) && subtype (tyT->_ty0, tyS->_ty0)))
                result_ty = new Ty(TyRef, tyS->_ty0);
            else // Warning: this is incomplete... 
                 result_ty = new Ty(TySource, meet(tyS->_ty0, tyT->_ty0));
        }        
        else if (tyS->_typ == TySource && tyT->_typ == TySource)
            result_ty = new Ty(TySource, meet(tyS->_ty0, tyT->_ty0));
        else if (tyS->_typ == TyRef && tyT->_typ == TySource)
            result_ty = new Ty(TySource, meet(tyS->_ty0, tyT->_ty0));
        else if (tyS->_typ == TySource && tyT->_typ == TyRef)
            result_ty = new Ty(TySource, meet(tyS->_ty0, tyT->_ty0));
        else if (tyS->_typ == TySink && tyT->_typ == TySink)
            result_ty = new Ty(TySink, join(tyS->_ty0, tyT->_ty0));
        else if (tyS->_typ == TyRef && tyT->_typ == TySink)
            result_ty = new Ty(TySink, join(tyS->_ty0, tyT->_ty0));
        else if (tyS->_typ == TySink && tyT->_typ == TyRef)
            result_ty = new Ty(TySink, join(tyS->_ty0, tyT->_ty0));     
        else
            result_ty = new Ty(TyBot);
    }
    return result_ty;
}


Ty* getTypeFromContext(Term* t, int db_index) {
    Ty* result_ty;
    Binding* bind = getbinding(db_index);
    switch (bind->_binding_name){
       case VarBind:
            result_ty = bind->_ty;
            break;
        case TmAbbBind:
            if (bind->_ty->_typ == TyNone){
                showErrorMsg(t, "No type recorded for variable " + index2name(db_index));
                exit(1);
            }
            result_ty = bind->_ty;
            break;
        default:
            showErrorMsg(t, "getTypeFromContext: Wrong kind of binding for variable " + index2name(db_index));
            exit(1);
    }
    return result_ty;
}


void checkkindstar(Ty* ty){
    Kind* kn = kindOf(ty);
    if (kn->_kn_name != KnStar){
        cout << "Kind * expected" << endl;
        exit(1);
    }
}


Ty* typeOf(Term* t) {
    Ty* result_ty;
    Binding *binding, *bind0, *bind1;
    Ty *ty0, *ty1, *ty2, *tyT1, *tyTi;
    Kind* kn;
    FieldTys* ftys;
    typedef vector<Ty*> CaseTys;
    CaseTys* casetys;
    int i, j;
    switch (t->_t_name){
        case TmVar:
            result_ty = getTypeFromContext(t, t->_db_index);
            break;
        case TmAbs:
            checkkindstar(t->_ty0);
            binding = new Binding(VarBind, t->_ty0);
            _context.push_back(pair_sb(t->_var_str, binding));
            ty1 = typeOf(t->_term0);
            _context.pop_back();
            result_ty  = new Ty(TyArr, t->_ty0, typeShift(-1, ty1));
            break;
        case TmApp:
            ty0 = typeOf(t->_term0);
            ty1 = typeOf(t->_term1);
            ty0 = lcst(ty0);       
            if (ty0->_typ == TyArr){
                if (subtype(ty1, ty0->_ty0))
                    result_ty = ty0->_ty1;
                else{
                    showErrorMsg(t, "parameter type mismatch");
                    exit(1);
                }
            }
            else if (ty0->_typ == TyBot)
                result_ty = new Ty(TyBot);
            else{
                 showErrorMsg(t, "arrow type expected");
                 exit(1);
            }                
            break;
        case TmTrue:
        case TmFalse:
            result_ty  = new Ty(TyBool);
            break;
        case TmIf:
            if (subtype(typeOf(t->_term0), new Ty(TyBool)))
                result_ty = join(typeOf(t->_term1), typeOf(t->_term2));
            else {
                showErrorMsg(t, "guard of conditional not a boolean");
                exit(1);
            }
            break;
        case TmRecord:
            ftys = new FieldTys();
            for (int i = 0; i < t->_fields->size(); i++)
                ftys->push_back(new FieldTy( t->_fields->at(i)->_label, typeOf(t->_fields->at(i)->_term)));
            result_ty = new Ty(TyRecord, ftys);
            break;
        case TmProj:
            ty0 = lcst(typeOf(t->_term0));
            if (ty0->_typ == TyRecord){
                for (i = 0; i < ty0->_ftys->size(); i++){
                    if (ty0->_ftys->at(i)->_label == t->_label){
                        result_ty = ty0->_ftys->at(i)->_ty;
                        break;
                    }
                }
                if (i >= ty0->_ftys->size()){
                    showErrorMsg(t, "label "+t->_label+" not found");
                }    
            }
            else if (ty0->_typ == TyBot)
                result_ty = new Ty(TyBot);
            else{
                showErrorMsg(t, "Expected record type");
                exit(1);
            }
            break;
        case TmLet:
            binding = new Binding(VarBind, typeOf(t->_term0));
            _context.push_back(pair_sb(t->_var_str, binding));
            result_ty  = typeShift (-1, typeOf(t->_term1));
            _context.pop_back();
            break;
        case TmFloat:
            result_ty  = new Ty(TyFloat);
            break;
        case TmTimesfloat:
            if (subtype(typeOf(t->_term0), new Ty(TyFloat)) && subtype(typeOf(t->_term1), new Ty(TyFloat)))
                result_ty  = new Ty(TyFloat);
            else {
                showErrorMsg(t, "argument of timesfloat is not a number");
                exit(1);
            }
            break;
        case TmCase:
            ty0 = lcst(typeOf(t->_term0));
            if (ty0->_typ == TyVariant){
                for (i = 0; i < t->_ccs->size(); i++){                    
                    for(j = 0; j < ty0->_ftys->size() ; j++)
                        if (t->_ccs->at(i)->_label == ty0->_ftys->at(j)->_label)
                            break;                              
                    if (j >= ty0->_ftys->size()){
                        showErrorMsg(t, "label "+t->_ccs->at(i)->_label+" not in type");
                        exit(1); 
                    }
                }
                casetys = new CaseTys();
                for (i = 0; i < t->_ccs->size(); i++){
                    for (j = 0; j < ty0->_ftys->size(); j++)
                        if(t->_ccs->at(i)->_label == ty0->_ftys->at(j)->_label){
                            tyTi = ty0->_ftys->at(j)->_ty;                            
                            binding = new Binding(VarBind, tyTi);
                            _context.push_back(pair_sb(t->_ccs->at(i)->_var_str, binding));
                            casetys->push_back(typeShift (-1, typeOf(t->_ccs->at(i)->_term)));
                            _context.pop_back();
                            break;                              
                        }
                        if (j >= ty0->_ftys->size()){
                            showErrorMsg(t, "label "+t->_ccs->at(i)->_label+" not found");
                            exit(1); 
                        }
                }
                result_ty = new Ty(TyBot);                
                for (i = 0; i < casetys->size(); i++)
                    result_ty = join(result_ty, casetys->at(i));
            }
            else if (ty0->_typ == TyBot)
                result_ty = new Ty(TyBot);
            else {
                showErrorMsg(t, "Expected variant type");
                exit(1);
            }
            break;
        case TmTag:
            ty0 = simplifyty(t->_ty0);
            if (ty0->_typ == TyVariant){
                for (i = 0; i < ty0->_ftys->size(); i++){
                    if(t->_label == ty0->_ftys->at(i)->_label){
                         if (subtype(typeOf(t->_term0), ty0->_ftys->at(i)->_ty)){
                            result_ty = t->_ty0;
                            break;
                         }
                         else {
                            showErrorMsg(t, "field does not have expected type");
                            exit(1);
                         }
                    }
                }
                if (i >= ty0->_ftys->size()) {
                    showErrorMsg(t, "label "+t->_var_str+" not found");
                    exit(1);
                }
            }
            else {
                showErrorMsg(t, "Annotation is not a variant type");
                exit(1);
             }
             break;                     
        case TmAscribe:
            checkkindstar(t->_ty0);
            if (subtype(typeOf(t->_term0), t->_ty0))
                result_ty = t->_ty0;
            else {
                showErrorMsg(t, "body of as-term does not have the expected type");
                exit(1);
            }
            break;
        case TmString:
            result_ty  = new Ty(TyString);
            break;
        case TmUnit:
            result_ty  = new Ty(TyUnit);
            break;
        case TmInert:
            result_ty  = t->_ty0;
            break;
        case TmFix:
            ty0 = lcst(typeOf(t->_term0));
            if (ty0->_typ == TyArr){
                if (subtype(ty0->_ty1, ty0->_ty0))
                    result_ty = ty0->_ty1;
                else {
                    showErrorMsg(t, "result of body not compatible with domain");
                    exit(1);
                }
            }
            else if (ty0->_typ == TyBot)
                result_ty = new Ty(TyBot);
            else {
                showErrorMsg(t, "arrow type expected");
                exit(1);
            }
            break;
        case TmRef:
            result_ty  = new Ty(TyRef, typeOf(t->_term0));
            break;
        case TmLoc:
            showErrorMsg(t, "locations are not supposed to occur in source programs!");
            exit(1);
            break;
        case TmDeref:
            ty0 = lcst(typeOf(t->_term0));
            if (ty0->_typ == TyRef)
                result_ty = ty0->_ty0;
            else if (ty0->_typ == TyBot)
                result_ty = new Ty(TyBot);
            else if (ty0->_typ == TySource)
                result_ty = ty0->_ty0;
            else {
                showErrorMsg(t, "argument of ! is not a Ref or Source");
                exit(1);
            }
            break;
        case TmAssign:
            ty0 = lcst(typeOf(t->_term0));
            if (ty0->_typ == TyRef){
                if(subtype(typeOf(t->_term1), ty0->_ty0))
                    result_ty = new Ty(TyUnit);
                else {
                    showErrorMsg(t, "arguments of := are incompatible");
                    exit(1);
                }
            }
            else if (ty0->_typ == TyBot){
                typeOf(t->_term1);
                result_ty = new Ty(TyBot);
            }
            else if (ty0->_typ == TySink){
                if(subtype(typeOf(t->_term1), ty0->_ty0))
                    result_ty = new Ty(TyUnit);
                else {
                    showErrorMsg(t, "arguments of := are incompatible");
                    exit(1);
                }
            }
            else {
                showErrorMsg(t, "argument of ! is not a Ref or Sink");
                exit(1);
            }
            break;
        case TmError:
            result_ty = new Ty(TyBot);
            break;
        case TmTAbs:
            binding = new Binding(TyVarBind, t->_ty0);
            _context.push_back(pair_sb(t->_u_var_str, binding));
            result_ty  = new Ty(TyAll, t->_u_var_str, t->_ty0, typeOf(t->_term0));          
            _context.pop_back();
            break;        
        case TmTApp:
            ty0 = typeOf(t->_term0);
            ty0 = lcst(ty0);
            if (ty0->_typ == TyAll){
                if (!subtype(t->_ty0, ty0->_ty0)){
                    showErrorMsg(t, "type parameter type mismatch");
                    exit(1);
                }
                result_ty = typeSubstTop(t->_ty0, ty0->_ty1);
            }
            else{
                 showErrorMsg(t, "universal type expected");
                 exit(1);
            }               
            break;        
        case TmTry:
            result_ty = join(typeOf(t->_term0), typeOf(t->_term1));
            break;
        case TmZero:
            result_ty  = new Ty(TyNat);
            break;  
        case TmSucc:
        case TmPred:
            if(subtype(typeOf(t->_term0), new Ty(TyNat)))
                result_ty  = new Ty(TyNat);
            else {
                showErrorMsg(t, "argument of succ is not a number");
                exit(1);
            }
            break;
        case TmIsZero:
            if(subtype(typeOf(t->_term0), new Ty(TyNat)))
                result_ty  = new Ty(TyBool);
            else {
                showErrorMsg(t, "argument of iszero is not a number");
                exit(1);
            }
            break;                   
        case TmPack:
            checkkindstar(t->_ty1);
            ty0 = simplifyty(t->_ty1);
            if (ty0->_typ == TySome){
                if (!subtype(t->_ty0, ty0->_ty0)){
                    showErrorMsg(t, "hidden type not a subtype of bound");
                    exit(1);
                }
                ty1 = typeOf(t->_term0);
                ty2 = typeSubstTop(t->_ty0, ty0->_ty1);
                if (subtype(ty1,ty2))
                    result_ty = t->_ty1;
                else{
                    showErrorMsg(t, "doesn't match declared type");
                    exit(1);                 
                }
            }
            else {
                showErrorMsg(t, "existential type expected");
                exit(1);
            }
            break;
        case TmUnpack:
            ty0 = lcst(typeOf(t->_term0));
            if (ty0->_typ == TySome){
                bind0 = new Binding(TyVarBind, ty0->_ty0);
                _context.push_back(pair_sb(t->_u_var_str, bind0));
                bind1 = new Binding(VarBind, ty0->_ty1);
                _context.push_back(pair_sb(t->_var_str, bind1));
                ty1 = typeOf(t->_term1);
                result_ty = typeShift(-2, ty1);
                _context.pop_back();
                _context.pop_back();
            }
            else {
                showErrorMsg(t, "existential type expected");
                exit(1);
            }
            break;
                                 
        default:
            break;
    }        
    return result_ty;
}


Kind* getkind(int i) {
    Kind* result_kn;
    Binding* b = getbinding(i);
    switch (b->_binding_name){
        case TyVarBind:
            result_kn = kindOf(b->_ty);
            break;
        case TyAbbBind:
            if(b->_kn->_kn_name != KnNone)
                result_kn = b->_kn;
            else{
                cout << "No kind recorded for variable " <<  index2name(i) << endl;
                exit(1);
            }
            break;
        default:
            cout << "getkind: Wrong kind of binding for variable " <<  index2name(i) << endl;
            exit(1);
            break;
    }
    return result_kn;
}


Kind* kindOf(Ty* ty) {
    Kind *result_kn, *knK0, *knK1;
    Binding* bind;
    FieldTys* ftys;
    int i;
    switch (ty->_typ){
        case TyRecord:
        case TyVariant:
            ftys = new FieldTys();
            for (i = 0; i < ty->_ftys->size(); i++){
                if (kindOf(ty->_ftys->at(i)->_ty)->_kn_name != KnStar){
                    cout << "Kind * expected" << endl;
                    exit(1);
                }
            }
            result_kn = new Kind(KnStar);
            break;
        case TyVar:
            result_kn = getkind(ty->_db_index);
            break;
        case TyAll:
        case TySome:
            bind = new Binding(TyVarBind, ty->_ty0);
            _context.push_back(pair_sb(ty->_u_var_str, bind));
            knK1 = kindOf(ty->_ty1);
            if (knK1->_kn_name != KnStar){
                cout << "Kind * expected" << endl;
                exit(1);
            }
            else
                result_kn = new Kind(KnStar);
            _context.pop_back();
            break; 
         case TyAbs:
            bind = new Binding(TyVarBind, maketop(ty->_kn0));
            _context.push_back(pair_sb(ty->_u_var_str, bind));
            knK1 = kindOf(ty->_ty0);
            result_kn = new Kind(KnArr, ty->_kn0, knK1);
            _context.pop_back();
            break; 
        case TyApp:
            knK0 = kindOf(ty->_ty0);
            knK1 = kindOf(ty->_ty1);
            if (knK0->_kn_name == KnArr){
                if (knK1->getKind_str() == knK0->_kn0->getKind_str())
                    result_kn = knK0->_kn1;
                else{
                    cout << "parameter kind mismatch" << endl;
                    exit(1);
                }
            }
            else{
                cout << "arrow kind expected" << endl;
                exit(1);
            }
            break;  
        case TyArr:
            if (kindOf(ty->_ty0)->_kn_name != KnStar){
                cout << "star kind expected" << endl;
                exit(1);
            }
            else if (kindOf(ty->_ty1)->_kn_name != KnStar){
                cout << "star kind expected" << endl;
                exit(1);
            }
            else
                result_kn = new Kind(KnStar);
            break;
         case TyRef:
         case TySource:
         case TySink:
            if (kindOf(ty->_ty0)->_kn_name != KnStar){
                cout << "star kind expected" << endl;
                exit(1);
            }
            else
                result_kn = new Kind(KnStar);
            break;
        default:
            result_kn = new Kind(KnStar);
            break;
    }
    return result_kn;    
}


Binding* checkbinding(Binding* b){
    Binding* result_bind;
    Ty* ty;
    Kind* kn;
    switch (b->_binding_name){
        case NameBind:
            result_bind = b;
            break;
        case TyVarBind:
            kindOf(b->_ty);
            result_bind = b;
            break;
        case VarBind:
            result_bind = b;
            break;
        case TyAbbBind:
            if (b->_kn->_kn_name == KnNone)
                result_bind = new Binding(TyAbbBind, b->_ty, kindOf(b->_ty));
            else{
                kn =  kindOf(b->_ty);               
                if (kn->_kn_name == b->_kn->_kn_name)
                    result_bind = b;
                else{
                    cout << "Kind of binding does not match declared kind" << endl;
                    exit(1);
                }
            }
            break;
        case TmAbbBind:
            if (b->_ty->_typ == TyNone){
                result_bind = new Binding(TmAbbBind, b->_term, typeOf(b->_term));
            }
            else{
                if (subtype(typeOf(b->_term), b->_ty))
                    result_bind = b;
                else{
                    cout << "Type of binding does not match declared type" << endl;
                    exit(1);
                }
            }
            break;
    }
    return result_bind;        
}

