text: #include "fullsub.h"
  
  /* ------------------------   Context management  ------------------------ */
  
  vector<pair_sb> _context ={};
  vector<pair_sb>* _context_ptr = &_context;
  
  
  string index2name(int db_index){
      int context_size = _context_ptr->size();
      if (db_index < 0 || _context_ptr->size() - 1 < db_index){
          cout << "Variable lookup failure: offset:" << db_index << "context size:" << context_size << endl;
          exit(1);
      }
      return  _context_ptr->at(_context_ptr->size() - db_index -1).first;
  }
  
  
  bool isnamebound(string v_str) {
      bool result_b = false;
      auto itr = _context_ptr->rbegin();
      for(; itr != _context_ptr->rend(); ++itr) {
          if (itr->first == v_str){                
              result_b = true;              
              break;
          }
      }
      return result_b;
  }
  
  
  string pickfreshname(string v_str){
      string result_str = v_str;
      if (isnamebound(v_str))
          result_str = pickfreshname(v_str + "'");
      else{
          _context.push_back(pair_sb(v_str, new Binding(NameBind)));
          result_str =  v_str;
      }    
      return result_str;
  }
  
  
  int name2index(string var_str){
      int index;
      auto itr = _context_ptr->rbegin();
      for(; itr != _context_ptr->rend(); ++itr) {
          if (itr->first == var_str){                
              index = distance(_context_ptr->rbegin(), itr);               
              break;
          }
      }
      if (itr == _context_ptr->rend()){
          cout << "Identifier \'" << var_str << "\' is unbound" << endl;
          exit(1);           
      }
      return index;
  }
  
  
  string succPr(int n, Term* succ_t) {
      if (succ_t->_term0->_t_name == TmZero)
          return to_string(n);
      else if (succ_t->_term0->_t_name == TmSucc)
          return succPr(n + 1, succ_t->_term0);
      else
          return "(succ " + succ_t->_term0->getTerm_str() + ")";
  }
  
  
  /* ------------------------   class member functions  ------------------------ */
  
  string Term::getTerm_str() {
      string result_str;
      string ty_str;
      vector<Field*>::iterator itr;
      vector<Ccase*>::iterator itr_ccs;
      string v_str;
      Binding* binding;    
      switch (_t_name) {
          case TmVar:
              result_str = index2name(_db_index);
              break;
          case TmAbs:
              ty_str =_ty->getTy_str();
              v_str = pickfreshname(_var_str);
              result_str = "(lambda " + v_str + ":" + ty_str +  ". " + _term0->getTerm_str() + ")";
              _context.pop_back();
              break;
          case TmApp:
              result_str = "(" + _term0->getTerm_str() + " " + _term1->getTerm_str() + ")";
              break;
          case TmUnit:
              result_str = "unit";
              break;
          case TmString:
              result_str =  _var_str;
              break;
          case TmTrue:
              result_str = "true";
              break;
          case TmFalse:
              result_str = "false";
              break;
          case TmZero:
              result_str = "0";
              break;
          case TmFloat:
              result_str = _var_str;
              break;
          case TmTimesfloat:
              result_str = "timesfloat " + _term0->getTerm_str() + " " +   _term1->getTerm_str();
              break;            
          case TmLet:
              v_str = _term0->getTerm_str();
              binding = new Binding(NameBind);
              _context.push_back(pair_sb( _var_str, binding));
              result_str = "let " + _var_str + " = " + v_str + " in " + _term1->getTerm_str();
              _context.pop_back();
              break;
          case TmIf:
              result_str = "if " + _term0->getTerm_str() + " then " +  _term1->getTerm_str()+ " else " +  _term2->getTerm_str();
              break;
          case TmSucc:
             result_str = succPr(1, this); 
              break;
          case TmPred:
              result_str = "(pred " + _term0->getTerm_str() + ")";
              break;
          case TmIsZero:
              result_str = "(iszero " + _term0->getTerm_str() + ")";
              break;
          case TmRecord:
              result_str = "{";
              for(itr = _fields->begin(); itr != _fields->end(); ++itr){
                  if (to_string(distance( _fields->begin(), itr)+ 1) == (*itr)->_label)
                      result_str += (*itr)->_term->getTerm_str();
                  else
                      result_str += (*itr)->_label + "=" + (*itr)->_term->getTerm_str();
                  if ((itr + 1) != _fields->end())
                      result_str += ", ";
              }                
              result_str += "}";
              break;
          case TmFix:
              result_str = "fix " + _term0->getTerm_str();
              break;
          case TmAscribe:
              result_str = _term0->getTerm_str() + " as " + _ty->getTy_str();
              break;
          case TmProj:
              result_str = _term0->getTerm_str() + "." + _label;
              break;
          case TmInert:
              result_str = "inert[" + _ty->getTy_str() + "]";   
              break;
      }
      return result_str;
  }       
  
  
  string Ty::getTy_str() {
      string result_str;
      switch (_typ) {
          case TyUnit:
              result_str = "Unit";
              break;
          case TyString:
              result_str = "String";
              break;
          case TyBool:
              result_str = "Bool";
              break;
          case TyTop:
              result_str = "Top";
              break;
          case TyNat:
              result_str = "Nat";
              break;
          case TyFloat:
              result_str = "Float";
              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 TyVar:
              result_str = index2name(_db_index);
              break;
          case TyId:
              result_str = _u_var_str;
              break;
          case TyError:
              result_str = "Type Error";
              break;                
      }
      return result_str;
  }      
  
  
  string Binding::getBing_str() {
      string result_str;
      switch (_binding_name){
          case NameBind:
              result_str = "";
              break;
          case VarBind:
              result_str = ":" + _ty->getTy_str(); 
              break;
          case TmAbbBind:
              if (_ty->_typ == TyNone)
                  result_str = ":" + typeOf(_term)->getTy_str(); 
              else
                  result_str = ":" + _ty->getTy_str();
              break;
          case TyVarBind:
              result_str = "";
              break;
          case TyAbbBind:
              result_str = ":: *";
              break; 
      }
      return result_str;
  }
  
  void showErrorMsg(Term* t, string msg) { cout << t->_info << + ": error: " + msg << endl; }
  
  
  /************************** copy functions ******************************/
  
  Term* copyTerm(Term* t){
      Term* result_t;
      Fields* fs;
      Ccases* ccs;
      int i;
      switch (t->_t_name) {
          case TmVar:
              result_t = new Term(t->_t_name, t->_info, t->_db_index);
              break;
          case TmAbs:
              result_t = new Term(t->_t_name, t->_info, t->_var_str, copyTy(t->_ty), copyTerm(t->_term0));
              break;
          case TmApp:
          case TmTimesfloat:
              result_t = new Term(t->_t_name, t->_info, copyTerm(t->_term0), copyTerm(t->_term1));
              break;
          case TmTrue:
          case TmFalse:
          case TmZero:
          case TmUnit:
              result_t = new Term(t->_t_name, t->_info);
              break;
          case TmString: 
          case TmFloat:
              result_t = new Term(t->_t_name, t->_info, t->_var_str);
              break;
          case TmSucc:
          case TmPred:
          case TmIsZero:
          case TmFix:
              result_t = new Term(t->_t_name, t->_info, copyTerm(t->_term0));
              break;
          case TmIf:
              result_t = new Term(t->_t_name, t->_info, copyTerm(t->_term0), copyTerm(t->_term1), copyTerm(t->_term2));
              break;
          case TmLet:
              result_t = new Term(t->_t_name, t->_info, t->_var_str, copyTerm(t->_term0), copyTerm(t->_term1));
              break;
          case TmRecord:
              fs = new Fields();
              for (i = 0; i < t->_fields->size(); i++)
                  fs->push_back(copyField(t->_fields->at(i)));
              result_t = new Term(TmRecord, t->_info, fs);
              break;
          case TmProj:
              result_t = new Term(t->_t_name, t->_info, copyTerm(t->_term0), t->_label);
              break;       
          case TmAscribe:
              result_t = new Term(TmAscribe, t->_info, copyTerm(t->_term0), copyTy(t->_ty));
              break;
          case TmInert:
              result_t = new Term(TmInert, t->_info, copyTy(t->_ty));
              break;
      }
      return result_t;
  }
  
  
  Field* copyField(Field* f) { return new Field( f->_label, copyTerm(f->_term));}
  
  
  Ty* copyTy(Ty* ty){
      Ty* result_ty;
      FieldTys* ftys;
      switch (ty->_typ) {
          case TyUnit:
          case TyBool:
          case TyTop:
          case TyNat:
          case TyFloat:
          case TyNone:
          case TyString:
          case TyError:
          case TYNoRuleApplies:
          case Ty_Not_found:
              result_ty = new Ty(ty->_typ);
              break;
          case TyArr:
              result_ty = new Ty(TyArr, copyTy(ty->_ty0), copyTy(ty->_ty1));
              break;
          case TyRecord:
              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;
      }
      return result_ty;
  }
  
  
  FieldTy* copyFieldTy(FieldTy* fty) { return new FieldTy(fty->_label, copyTy(fty->_ty));}
  
  
  Binding* copyBinding(Binding* b){
      Binding* result_bind;
      switch (b->_binding_name){
          case NameBind:
          case TyVarBind:
              result_bind = new Binding(b->_binding_name);
              break;
          case VarBind:
          case TyAbbBind:
              result_bind = new Binding(b->_binding_name, copyTy(b->_ty));
              break;
          case TmAbbBind:
              result_bind = new Binding(TmAbbBind, copyTerm(b->_term), copyTy(b->_ty));
              break;
      }
      return result_bind;
  }
  
  
  /* ------------------------   Shifting  ------------------------ */
  
  Term* termShiftAbove(int d, int c, Term* t) {
      Term* result_t;    
      Fields* fs;    
      switch (t->_t_name) {
          case TmAscribe:
              t->_term0 = termShiftAbove(d, c, t->_term0);
              t->_ty = typeShiftAbove(d, c, t->_ty);
              result_t = t;
              break;
          case TmVar:
              if (t->_db_index >= c)
                  t->_db_index += d; 
              result_t = t;
              break;
          case TmAbs:
              t = copyTerm(t);
              t->_term0 = termShiftAbove(d, c + 1, t->_term0);
              t->_ty = typeShiftAbove(d, c, t->_ty);
              result_t = t;
              break;
          case TmApp:
          case TmTimesfloat:
              t->_term0 = termShiftAbove(d, c, t->_term0);
              t->_term1 = termShiftAbove(d, c, t->_term1);
              result_t = t;
              break;
          case TmSucc:
          case TmPred:
          case TmIsZero:
              t->_term0 = termShiftAbove(d, c, t->_term0);
              result_t = t;
              break;
          case TmZero:
          case TmUnit:
          case TmTrue:
          case TmFalse:
          case TmString:
          case TmFloat:
              result_t = t;                
              break;
          case TmInert:
              t->_ty = typeShiftAbove(d, c, t->_ty);
              result_t = t;
              break;
           case TmIf:
              t->_term0 = termShiftAbove(d, c, t->_term0);
              t->_term1 = termShiftAbove(d, c, t->_term1);
              t->_term2 = termShiftAbove(d, c, t->_term2);
              result_t = t;
              break;
          case TmLet:
              t->_term0 = termShiftAbove(d, c, t->_term0);
              t->_term1 = termShiftAbove(d, c + 1, t->_term1);
              result_t = t;
              break;
          case TmRecord:
              fs = new Fields();
              for (int i = 0; i < t->_fields->size(); i++)
                  t->_fields->at(i)->_term = termShiftAbove(d, c, t->_fields->at(i)->_term);
              result_t = t;
              break;
          case TmFix:
          case TmProj:
              t->_term0 = termShiftAbove(d, c, t->_term0);
              result_t = t;
              break;
      }
      return result_t;
  }
  
  
  Term* termShift(int d, Term* t) {
      return termShiftAbove(d, 0, t); 
  }
  
  
  /* ------------------------   Substitution  ------------------------ */
  
  Term* termSubst(int var_num, Term* s_term, Term* t) {
      Term* result_t;
      Term *t0, *t1, *t2;
      Field* f;
      Fields* fs;
      switch (t->_t_name) {
          case TmAscribe:
              t0 = termSubst(var_num, s_term, t->_term0);
              result_t = new Term(TmAscribe, t->_info, t0, t->_ty);
              break;
          case TmVar:
              if (t->_db_index == var_num){
                  result_t = termShift(t->_db_index, s_term);
              }
              else
                  result_t = new Term(TmVar, t->_info, t->_db_index);
              break;
          case TmAbs:
              t0 = termSubst(var_num + 1, s_term, t->_term0);
              result_t = new Term(TmAbs, t->_info, t->_var_str, t->_ty, t0);
              break;
          case TmApp:
              t0 = termSubst(var_num, s_term, t->_term0);
              t1 = termSubst(var_num, s_term, t->_term1);
              result_t = new Term(TmApp, t->_info, t0, t1);
              break;
          case TmTimesfloat:
              t0 = termSubst(var_num, s_term, t->_term0);
              t1 = termSubst(var_num, s_term, t->_term1);
              result_t = new Term(TmTimesfloat, t->_info, t0, t1);
              break;
          case TmSucc:
          case TmPred:
          case TmIsZero:
              t0 = termSubst(var_num, s_term, t->_term0);
              result_t = new Term(t->_t_name, t->_info, t0);
              break;
          case TmUnit:           
          case TmTrue:
          case TmFalse:
          case TmZero:
              result_t = new Term(t->_t_name, t->_info);
              break;
          case TmString:
          case TmFloat:
              result_t = new Term(t->_t_name, t->_info, t->_var_str);
              break; 
          case TmInert:
              result_t = new Term(TmInert, t->_info, t->_ty);
              break;          
          case TmIf:
              t0 = termSubst(var_num, s_term, t->_term0);
              t1 = termSubst(var_num, s_term, t->_term1);
              t2 = termSubst(var_num, s_term, t->_term2);
              result_t = new Term(TmIf, t->_info, t0, t1, t2);
              break;
          case TmLet:
              t0 = termSubst(var_num, s_term, t->_term0);
              t1 = termSubst(var_num + 1, s_term, t->_term1);
              result_t = new Term(TmLet, t->_info, t->_var_str, t0, t1);
              break;
          case TmRecord:
              fs = new Fields();
              for (int i = 0; i < t->_fields->size(); i++){
                  f = new Field( t->_fields->at(i)->_label, termSubst(var_num, s_term, t->_fields->at(i)->_term));
                  fs->push_back(f);
              }
              result_t = new Term(TmRecord, t->_info, fs);
              break;
          case TmFix:
              t0 = termSubst(var_num, s_term, t->_term0);
              result_t = new Term(TmFix, t->_info, t0);
              break;
          case TmProj:
              t0 = termSubst(var_num, s_term, t->_term0);
              result_t = new Term(t->_t_name, t->_info, t0, t->_label);
              break;
      }        
      return result_t;
  }
  
  
  Term* termSubstTop(Term* s_term, Term* t) { return termShift(-1, termSubst(0, termShift(1, s_term), t));}
  
  
  
  /* ------------------------   TYPING  ------------------------ */
  
  Ty* typeShiftAbove(int d, int c, Ty* ty) {
      Ty* result_ty;
      FieldTys* ftys;
      FieldTy* fty;
      Ty* ty0;
      int i;
      switch (ty->_typ){
          case TyArr:
              result_ty = new Ty(TyArr, typeShiftAbove(d, c, ty->_ty0),  typeShiftAbove(d, c, ty->_ty1));
              break;
          case TyUnit:
          case TyBool:
          case TyNat:
          case TyString:
          case TyFloat:
          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:
              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;
      }
      return result_ty;
  }
  
  
  Ty* typeShift(int d, Ty* ty){ return typeShiftAbove(d, 0, ty);}
  
  
  Binding* bindingshift(int d, Binding* bind) {
      Binding* result_bind;
      Term* t;
       switch (bind->_binding_name){
          case NameBind:
          case TyVarBind:
              result_bind = new Binding(bind->_binding_name);
              break;
          case TmAbbBind:
              t = termShift(d, bind->_term);
              if (bind->_ty->_typ == TyNone)
                  result_bind = new Binding(TmAbbBind, t, new Ty(TyNone));
              else{
                  result_bind = new Binding(TmAbbBind, t, typeShift(d, bind->_ty));
              }
              break;
          case VarBind:
          case TyAbbBind:
              result_bind = new Binding(bind->_binding_name, typeShift(d, bind->_ty));
              break;         
       }
       return result_bind;
  }
  
  
  Binding* getbinding (int db_index){
      int context_size = _context_ptr->size();
      if (db_index < 0 || _context_ptr->size() - 1 < db_index){
          cout << "getbinding :Variable lookup failure: offset:" << db_index << "context size:" << context_size << endl;
          exit(1);
      }
      Binding* b = _context_ptr->at(_context_ptr->size() - db_index -1).second;
      return bindingshift(db_index + 1, copyBinding(b));
  }
  
  
  Binding* evalbinding(Binding* b){
      Binding* result_bind = b;
      bool NoRuleApplies = false;
      if (b->_binding_name == TmAbbBind){
          b->_term = eval(b->_term, &NoRuleApplies);
          result_bind = b;
      }
       return result_bind;
  }
  
  
  bool istyabb(int i){
      bool result_b = false;
      Binding* b = getbinding(i);
      if (b->_binding_name == TyAbbBind)
          result_b = true;
      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
          result_ty = new Ty(TYNoRuleApplies);
      return result_ty;
  
  }
  
  
  Ty* simplifyty(Ty* ty) {
      Ty* ty1 = computety(ty);
      if (ty1->_typ != TYNoRuleApplies)
          return simplifyty(ty1);
      else
          return ty;
  }
  
  
  bool tyeqv (Ty* ty0, Ty* ty1) {
      bool result_b = false;
      int i, j;
      Ty* tyS = simplifyty(ty0);
      Ty* tyT = simplifyty(ty1);
      if (tyS->_typ == TyUnit && tyT->_typ == TyUnit)
          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 == TyFloat && tyT->_typ == TyFloat)
          result_b = true;
      else 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 == 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){
          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 (!result_b || j >= tyS->_ftys->size()){
                      result_b = false;
                      break;
                  }
                  
              }
          }
      }    
      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
          result_b = false;
      return result_b;
  }
  
  bool subtype (Ty* ty0, Ty* ty1) {
      bool result_b;
      int i, j;
      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 == 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 (!result_b || j >= tyS->_ftys->size()){
                      result_b = false;
                      break;
                  }
              }
          }
          else if (tyS->_typ == TyArr && tyT->_typ == TyArr)
              result_b = subtype (tyT->_ty0, tyS->_ty0) && subtype (tyS->_ty1, tyT->_ty1);
          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;
      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 == TyArr && tyT->_typ == TyArr){
              meet_ty = meet(tyS->_ty0, tyT->_ty0);
              if (meet_ty->_typ != Ty_Not_found ) 
                  result_ty  = new Ty(TyArr, meet_ty, join(tyS->_ty1, tyT->_ty1));
              else
                  result_ty  = new Ty(TyTop);
          }
          else
              result_ty  = new Ty(TyTop);
      }
      return result_ty;
  }
  
  
  Ty* meet (Ty* ty0, Ty* ty1) {
      Ty* result_ty;
      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 (int i = 0; i < allLabels->size(); i++) {
                  for (int j = 0; j < tyS->_ftys->size(); j++) 
                      if (allLabels->at(i) == tyS->_ftys->at(j)->_label){
                          tySi = tyS->_ftys->at(j)->_ty;
                          break;
                      }
                  for (int 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 == TyArr && tyT->_typ == TyArr)
              result_ty  = new Ty(TyArr, join(tyS->_ty0, tyT->_ty0), meet(tyS->_ty1, tyT->_ty1));    
          else
              result_ty = new Ty(Ty_Not_found);
      }
      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;
  }
  
  
  Ty* typeOf(Term* t) {
      Ty* result_ty;
      Binding* binding;
      Ty *ty0, *ty1, *ty2, *tyT1, *tyTi;
      FieldTys* ftys;
      
      int i, j;
      bool NoRuleApplies;
      switch (t->_t_name){
          case TmAscribe:
               if (subtype(typeOf(t->_term0), t->_ty))
                  result_ty = t->_ty;
              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 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 = simplifyty(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");
                      exit(1);
                  }    
              }
              else{
                  showErrorMsg(t, "Expected record type");
                  exit(1);
              }
              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 TmVar:
              result_ty = getTypeFromContext(t, t->_db_index);
              break; 
          case TmAbs:
              binding = new Binding(VarBind, t->_ty);
              _context.push_back(pair_sb(t->_var_str, binding));
              result_ty  = new Ty(TyArr, t->_ty, typeShift(-1, typeOf(t->_term0)));          
              _context.pop_back();
              break;   
          case TmApp:
              ty1 = typeOf(t->_term1);
              ty0 = simplifyty(typeOf(t->_term0));
              NoRuleApplies = false;
              if (ty0->_typ == TyArr)
                  if (subtype(ty1, ty0->_ty0))
                      result_ty = ty0->_ty1;
                  else{
                      showErrorMsg(t, "parameter type mismatch");
                      exit(1);
                  }
              else{
                   showErrorMsg(t, "arrow type expected");
                   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 TmInert:
              result_ty  = t->_ty;
              break;
          case TmFix:
              ty0 = simplifyty(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 {
                  showErrorMsg(t, "arrow type expected");
                  exit(1);
              }
              break;     
          case TmZero:
              result_ty  = new Ty(TyNat);
              break;  
          case TmSucc:
              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 TmPred:
              if (subtype(typeOf(t->_term0), new Ty(TyNat)))
                  result_ty  = new Ty(TyNat);
              else {
                  showErrorMsg(t, "argument of pred 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;
          
          default:
              break;
      }        
      return result_ty;
  }
  
  
  Binding* checkbinding(Binding* b){
      Binding* result_bind;
      Ty* ty;
      switch (b->_binding_name){
          case NameBind:
          case VarBind:
          case TyAbbBind:
          case TyVarBind:
              result_bind = b;
              break;
          case TmAbbBind:
              if (b->_ty->_typ == TyNone){
                  result_bind = new Binding(TmAbbBind, b->_term, typeOf(b->_term));
              }
              else{
                  ty = typeOf(b->_term);
                  if (tyeqv(ty, b->_ty))
                      result_bind = b;
                  else{
                      cout << "Type of binding does not match declared type" << endl;
                      exit(1);
                  }
              }
              break;
      }
      return result_bind;        
  }
  
  
  
  /* ------------------------   EVALUATION  ------------------------ */
  
  bool isnumericval(Term* t) {
      bool result_b;
      switch (t->_t_name){
          case TmZero:
              result_b = true;
              break;
          case TmSucc:
              result_b = isnumericval(t->_term0);
              break;
          default:
              result_b = false;
              break;
      }  
      return result_b;      
  }
  
  
  bool isval(Term* t) {
      bool result_b;
      switch(t->_t_name){
          case TmString:
          case TmUnit:
          case TmTrue:
          case TmFalse:
          case TmAbs: 
          case TmFloat:
              result_b = true;
              break;
          case TmRecord:        
              result_b = all_of(t->_fields->begin(), t->_fields->end(), [](Field* f){return isval(f->_term);});
              break;
          default:
              if (isnumericval(t))
                  result_b = true;
              else
                  result_b = false;
              break;
      }
      return result_b;
  }
  
  
  Fields* evalafield(Fields* fs, int i, bool* NoRuleApplies) {
      Fields* result_fs;
      if (fs->size() <= 0 || fs->size() - 1 < i){
          *NoRuleApplies = true;
          result_fs = fs;
      }
      else if (isval(fs->at(i)->_term)){
          result_fs = evalafield(fs, i+1, NoRuleApplies);
      }
      else{
          fs->at(i)->_term = eval1(fs->at(i)->_term, NoRuleApplies);
          * NoRuleApplies = false;
          result_fs = fs; 
      }
      return result_fs;   
  }
  
  
  Term* eval1(Term* t, bool* NoRuleApplies){
      Term* result_t;
      Binding* b;
      Term* t0;
      int i;
      switch(t->_t_name){
          case TmAscribe:
              if (isval(t->_term0))
                  result_t = t->_term0;
              else{
                  t->_term0 = eval1(t->_term0, NoRuleApplies);
                  result_t = t;
              }              
              break;
          case TmSucc:
              t->_term0 = eval1(t->_term0, NoRuleApplies);
              result_t = t;
              break;              
          case TmPred:
              if (t->_term0->_t_name == TmZero)
                  result_t = new Term(TmZero, t->_info);
              else if (t->_term0->_t_name == TmSucc && isnumericval(t->_term0->_term0))
                  result_t = t->_term0->_term0;
              else{
                  t->_term0 = eval1(t->_term0, NoRuleApplies);
                  result_t = t;
              }
              break;
          case TmIsZero:
              if (t->_term0->_t_name == TmZero)
                  result_t = new Term(TmTrue, t->_info);
              else if (t->_term0->_t_name == TmSucc && isnumericval(t->_term0->_term0))
                  result_t = new Term(TmFalse, t->_info);
              else{
                  t->_term0 = eval1(t->_term0, NoRuleApplies);
                  result_t = t;
              }
              break;  
          case TmApp:
              if (t->_term0->_t_name == TmAbs && isval(t->_term1)){
                  result_t = termSubstTop(t->_term1, t->_term0->_term0);
              }
              else if (isval(t->_term0)){
                  t->_term1 = eval1(t->_term1, NoRuleApplies);
                  result_t = t;
              }
              else {
                  t->_term0 = eval1(t->_term0, NoRuleApplies);
                  result_t = t;             
              }
              break;
          case TmIf:
              if (t->_term0->_t_name == TmTrue)
                  result_t = t->_term1;
              else if (t->_term0->_t_name == TmFalse)
                  result_t = t->_term2;
              else{
                  t->_term0 = eval1(t->_term0, NoRuleApplies);
                  result_t = t;
              }
              break;
           case TmVar:
              b = getbinding(t->_db_index);
              if(b->_binding_name == TmAbbBind)              
                  result_t = b->_term;
              else{
                  result_t = t;
                  *NoRuleApplies = true;
              }
              break;
          case TmTimesfloat:
              if (t->_term0->_t_name == TmFloat && t->_term1->_t_name == TmFloat)
                  result_t = new Term(TmFloat, t->_info, to_string(stof(t->_term0->_var_str) * stof(t->_term1->_var_str)));
              else if (t->_term0->_t_name == TmFloat){
                   t->_term1 = eval1(t->_term1, NoRuleApplies);
                   result_t = t;
              }
              else {
                  t->_term0 = eval1(t->_term0, NoRuleApplies);
                  result_t = t;
              }
              break;
          case TmLet:
              if (isval(t->_term0))
                  result_t = termSubstTop(t->_term0, t->_term1);
              else{
                  t->_term0 = eval1(t->_term0, NoRuleApplies);
                  result_t = t;
              }
              break;
          case TmRecord:
              t->_fields = evalafield(t->_fields, 0, NoRuleApplies);
              result_t = t;
              break;
          case TmProj:
              t0 = t->_term0;
              if (t0->_t_name == TmRecord){
                  for (i = 0; i < t0->_fields->size(); i++){
                      if (t0->_fields->at(i)->_label == t->_label){
                          result_t = t0->_fields->at(i)->_term;
                          break;
                      }
                  }                    
                  if (i  == t0->_fields->size()){
                      showErrorMsg(t, "label "+t->_label+" not found");
                      exit(1);
                  }
              }
              else{
                  t->_term0 = eval1(t->_term0, NoRuleApplies);
                  result_t = t;
              }
              break;
          case TmFix:
              if (isval(t->_term0)){
                  if (t->_term0->_t_name == TmAbs)
                      result_t = termSubstTop(t, t->_term0->_term0);
                  else {
                      result_t = t;
                      *NoRuleApplies = true;
                  }                
              }
              else{
                  t->_term0 = eval1(t->_term0, NoRuleApplies);
                  result_t = t;
              }
              break;
          default:
              result_t = t;
              *NoRuleApplies = true;
              break;
      }        
      return result_t;
  }
  
  
  Term* eval(Term* t, bool* NoRuleApplies){
      if (*NoRuleApplies)           
          return t;
      else
          return eval(eval1(t, NoRuleApplies), NoRuleApplies);
  }
  
  