/*
 * This file is part of the Cforall project
 *
 * $Id: Unify.cc,v 1.14 2005/08/29 20:14:16 rcbilson Exp $
 *
 */

#include <set>
#include <memory>

#include "Unify.h"
#include "TypeEnvironment.h"
#include "typeops.h"
#include "FindOpenVars.h"
#include "SynTree/Visitor.h"
#include "SynTree/Type.h"
#include "SynTree/Declaration.h"
#include "SymTab/Indexer.h"
#include "utility.h"


//#define DEBUG

namespace ResolvExpr {

struct WidenMode
{
  WidenMode( bool widenFirst, bool widenSecond ): widenFirst( widenFirst ), widenSecond( widenSecond ) {}
  WidenMode &operator|=( const WidenMode &other ) { widenFirst |= other.widenFirst; widenSecond |= other.widenSecond; return *this; }
  WidenMode &operator&=( const WidenMode &other ) { widenFirst &= other.widenFirst; widenSecond &= other.widenSecond; return *this; }
  WidenMode operator|( const WidenMode &other ) { WidenMode newWM( *this ); newWM |= other; return newWM; }
  WidenMode operator&( const WidenMode &other ) { WidenMode newWM( *this ); newWM &= other; return newWM; }
  operator bool() { return widenFirst && widenSecond; }
  
  bool widenFirst : 1, widenSecond : 1;
};

class Unify : public Visitor
{
public:
  Unify( Type *type2, TypeEnvironment &env, AssertionSet &needAssertions, AssertionSet &haveAssertions, const OpenVarSet &openVars, WidenMode widenMode, const SymTab::Indexer &indexer );
  
  bool get_result() const { return result; }

private:
  virtual void visit(VoidType *voidType);
  virtual void visit(BasicType *basicType);
  virtual void visit(PointerType *pointerType);
  virtual void visit(ArrayType *arrayType);
  virtual void visit(FunctionType *functionType);
  virtual void visit(StructInstType *aggregateUseType);
  virtual void visit(UnionInstType *aggregateUseType);
  virtual void visit(EnumInstType *aggregateUseType);
  virtual void visit(ContextInstType *aggregateUseType);
  virtual void visit(TypeInstType *aggregateUseType);
  virtual void visit(TupleType *tupleType);

  template< typename RefType > void handleRefType( RefType *inst, Type *other );

  bool result;
  Type *type2;				// inherited
  TypeEnvironment &env;
  AssertionSet &needAssertions;
  AssertionSet &haveAssertions;
  const OpenVarSet &openVars;
  WidenMode widenMode;
  Type *commonType;
  const SymTab::Indexer &indexer;
};

bool unifyInexact( Type *type1, Type *type2, TypeEnvironment &env, AssertionSet &needAssertions, AssertionSet &haveAssertions, const OpenVarSet &openVars, WidenMode widenMode, const SymTab::Indexer &indexer, Type *&common );
bool unifyExact( Type *type1, Type *type2, TypeEnvironment &env, AssertionSet &needAssertions, AssertionSet &haveAssertions, const OpenVarSet &openVars, WidenMode widenMode, const SymTab::Indexer &indexer );
  
bool
typesCompatible( Type *first, Type *second, const SymTab::Indexer &indexer, const TypeEnvironment &env )
{
  TypeEnvironment newEnv;
  OpenVarSet openVars;
  AssertionSet needAssertions, haveAssertions;
  Type *newFirst = first->clone(), *newSecond = second->clone();
  env.apply( newFirst );
  env.apply( newSecond );
  bool result = unifyExact( newFirst, newSecond, newEnv, needAssertions, haveAssertions, openVars, WidenMode( false, false ), indexer );
  delete newFirst;
  delete newSecond;
  return result;
}

bool
typesCompatibleIgnoreQualifiers( Type *first, Type *second, const SymTab::Indexer &indexer, const TypeEnvironment &env )
{
  TypeEnvironment newEnv;
  OpenVarSet openVars;
  AssertionSet needAssertions, haveAssertions;
  Type *newFirst = first->clone(), *newSecond = second->clone();
  env.apply( newFirst );
  env.apply( newSecond );
  newFirst->get_qualifiers() = Type::Qualifiers();
  newSecond->get_qualifiers() = Type::Qualifiers();
///   std::cout << "first is ";
///   first->print( std::cout );
///   std::cout << std::endl << "second is ";
///   second->print( std::cout );
///   std::cout << std::endl << "newFirst is ";
///   newFirst->print( std::cout );
///   std::cout << std::endl << "newSecond is ";
///   newSecond->print( std::cout );
///   std::cout << std::endl;
  bool result = unifyExact( newFirst, newSecond, newEnv, needAssertions, haveAssertions, openVars, WidenMode( false, false ), indexer );
  delete newFirst;
  delete newSecond;
  return result;
}

bool
isFtype( Type *type, const SymTab::Indexer &indexer )
{
  if( dynamic_cast< FunctionType* >( type ) ) {
    return true;
  } else if( TypeInstType *typeInst = dynamic_cast< TypeInstType* >( type ) ) {
    return typeInst->get_isFtype();
  }
  return false;
}

bool
tyVarCompatible( TypeDecl::Kind kind, Type *type, const SymTab::Indexer &indexer )
{
  switch( kind ) {
  case TypeDecl::Any:
  case TypeDecl::Dtype:
    return !isFtype( type, indexer );
  
  case TypeDecl::Ftype:
    return isFtype( type, indexer );
  }
  assert( false );
  return false;
}

bool
bindVar( TypeInstType *typeInst, Type *other, TypeDecl::Kind kind, TypeEnvironment &env, AssertionSet &needAssertions, AssertionSet &haveAssertions, const OpenVarSet &openVars, WidenMode widenMode, const SymTab::Indexer &indexer )
{
  OpenVarSet::const_iterator tyvar = openVars.find( typeInst->get_name() );
  assert( tyvar != openVars.end() );
  if( !tyVarCompatible( tyvar->second, other, indexer ) ) {
    return false;
  }
  if( occurs( other, typeInst->get_name(), env ) ) {
    return false;
  }
  EqvClass curClass;
  if( env.lookup( typeInst->get_name(), curClass ) ) {
    if( curClass.type ) {
      Type *common = 0;
      std::auto_ptr< Type > newType( curClass.type->clone() );
      if( unifyInexact( newType.get(), other, env, needAssertions, haveAssertions, openVars, widenMode & WidenMode( curClass.allowWidening, true ), indexer, common ) ) {
        if( common ) {
          common->get_qualifiers() = Type::Qualifiers();
          delete curClass.type;
          curClass.type = common;
          env.add( curClass );
        }
        return true;
      } else {
        return false;
      }
    } else {
      curClass.type = other->clone();
      curClass.type->get_qualifiers() = Type::Qualifiers();
      curClass.allowWidening = widenMode.widenFirst && widenMode.widenSecond;
      env.add( curClass );
    }
  } else {
    EqvClass newClass;
    newClass.vars.insert( typeInst->get_name() );
    newClass.type = other->clone();
    newClass.type->get_qualifiers() = Type::Qualifiers();
    newClass.allowWidening = widenMode.widenFirst && widenMode.widenSecond;
    newClass.kind = kind;
    env.add( newClass );
  }
  return true;
}

bool
bindVarToVar( TypeInstType *var1, TypeInstType *var2, TypeDecl::Kind kind, TypeEnvironment &env, AssertionSet &needAssertions, AssertionSet &haveAssertions, const OpenVarSet &openVars, WidenMode widenMode, const SymTab::Indexer &indexer )
{
  bool result = true;
  EqvClass class1, class2;
  bool hasClass1 = false, hasClass2 = false;
  bool widen1 = false, widen2 = false;
  Type *type1 = 0, *type2 = 0;
  
  if( env.lookup( var1->get_name(), class1 ) ) {
    hasClass1 = true;
    if( class1.type ) {
      if( occurs( class1.type, var2->get_name(), env ) ) {
        return false;
      }
      type1 = class1.type->clone();
    }
    widen1 = widenMode.widenFirst && class1.allowWidening;
  }
  if( env.lookup( var2->get_name(), class2 ) ) {
    hasClass2 = true;
    if( class2.type ) {
      if( occurs( class2.type, var1->get_name(), env ) ) {
        return false;
      }
      type2 = class2.type->clone();
    }
    widen2 = widenMode.widenSecond && class2.allowWidening;
  }
  
  if( type1 && type2 ) {
//    std::cout << "has type1 && type2" << std::endl;
    WidenMode newWidenMode ( widen1, widen2 );
    Type *common = 0;
    if( unifyInexact( type1, type2, env, needAssertions, haveAssertions, openVars, newWidenMode, indexer, common ) ) {
      class1.vars.insert( class2.vars.begin(), class2.vars.end() );
      class1.allowWidening = widen1 && widen2;
      if( common ) {
        common->get_qualifiers() = Type::Qualifiers();
        delete class1.type;
        class1.type = common;
      }
      env.add( class1 );
    } else {
      result = false;
    }
  } else if( hasClass1 && hasClass2 ) {
    if( type1 ) {
      class1.vars.insert( class2.vars.begin(), class2.vars.end() );
      class1.allowWidening = widen1;
      env.add( class1 );
    } else {
      class2.vars.insert( class1.vars.begin(), class1.vars.end() );
      class2.allowWidening = widen2;
      env.add( class2 );
    }
  } else if( hasClass1 ) {
    class1.vars.insert( var2->get_name() );
    class1.allowWidening = widen1;
    env.add( class1 );
  } else if( hasClass2 ) {
    class2.vars.insert( var1->get_name() );
    class2.allowWidening = widen2;
    env.add( class2 );
  } else {
    EqvClass newClass;
    newClass.vars.insert( var1->get_name() );
    newClass.vars.insert( var2->get_name() );
    newClass.allowWidening = widen1 && widen2;
    newClass.kind = kind;
    env.add( newClass );
  }
  delete type1;
  delete type2;
  return result;
}

bool
unify( Type *type1, Type *type2, TypeEnvironment &env, AssertionSet &needAssertions, AssertionSet &haveAssertions, OpenVarSet &openVars, const SymTab::Indexer &indexer )
{
  OpenVarSet closedVars;
  findOpenVars( type1, openVars, closedVars, needAssertions, haveAssertions, false );
  findOpenVars( type2, openVars, closedVars, needAssertions, haveAssertions, true );
  Type *commonType = 0;
  if( unifyInexact( type1, type2, env, needAssertions, haveAssertions, openVars, WidenMode( true, true ), indexer, commonType ) ) {
    if( commonType ) {
      delete commonType;
    }
    return true;
  } else {
    return false;
  }
}

bool
unify( Type *type1, Type *type2, TypeEnvironment &env, AssertionSet &needAssertions, AssertionSet &haveAssertions, OpenVarSet &openVars, const SymTab::Indexer &indexer, Type *&commonType )
{
  OpenVarSet closedVars;
  findOpenVars( type1, openVars, closedVars, needAssertions, haveAssertions, false );
  findOpenVars( type2, openVars, closedVars, needAssertions, haveAssertions, true );
  return unifyInexact( type1, type2, env, needAssertions, haveAssertions, openVars, WidenMode( true, true ), indexer, commonType );
}

bool
unifyExact( Type *type1, Type *type2, TypeEnvironment &env, AssertionSet &needAssertions, AssertionSet &haveAssertions, const OpenVarSet &openVars, WidenMode widenMode, const SymTab::Indexer &indexer )
{
#ifdef DEBUG
  TypeEnvironment debugEnv( env );
#endif
  bool result;
  TypeInstType *var1 = dynamic_cast< TypeInstType* >( type1 );
  TypeInstType *var2 = dynamic_cast< TypeInstType* >( type2 );
  OpenVarSet::const_iterator entry1, entry2;
  if( var1 ) {
    entry1 = openVars.find( var1->get_name() );
  }
  if( var2 ) {
    entry2 = openVars.find( var2->get_name() );
  }
  bool isopen1 = var1 && ( entry1 != openVars.end() );
  bool isopen2 = var2 && ( entry2 != openVars.end() );
  if( type1->get_qualifiers() != type2->get_qualifiers() ) {
    return false;
  } else if( isopen1 && isopen2 && entry1->second == entry2->second ) {
    result = bindVarToVar( var1, var2, entry1->second, env, needAssertions, haveAssertions, openVars, widenMode, indexer );
  } else if( isopen1 ) {
    result = bindVar( var1, type2, entry1->second, env, needAssertions, haveAssertions, openVars, widenMode, indexer );
  } else if( isopen2 ) {
    result = bindVar( var2, type1, entry2->second, env, needAssertions, haveAssertions, openVars, widenMode, indexer );
  } else {
    Unify comparator( type2, env, needAssertions, haveAssertions, openVars, widenMode, indexer );
    type1->accept( comparator );
    result = comparator.get_result();
  }
#ifdef DEBUG
  std::cout << "============ unifyExact" << std::endl;
  std::cout << "type1 is ";
  type1->print( std::cout );
  std::cout << std::endl << "type2 is ";
  type2->print( std::cout );
  std::cout << std::endl << "openVars are ";
  printOpenVarSet( openVars, std::cout, 8 );
  std::cout << std::endl << "input env is " << std::endl;
  debugEnv.print( std::cout, 8 );
  std::cout << std::endl << "result env is " << std::endl;
  env.print( std::cout, 8 );
  std::cout << "result is " << result << std::endl;
#endif
  return result;
}

bool
unifyExact( Type *type1, Type *type2, TypeEnvironment &env, AssertionSet &needAssertions, AssertionSet &haveAssertions, OpenVarSet &openVars, const SymTab::Indexer &indexer )
{
  return unifyExact( type1, type2, env, needAssertions, haveAssertions, openVars, WidenMode( false, false ), indexer );
}

bool
unifyInexact( Type *type1, Type *type2, TypeEnvironment &env, AssertionSet &needAssertions, AssertionSet &haveAssertions, const OpenVarSet &openVars, WidenMode widenMode, const SymTab::Indexer &indexer, Type *&common )
{
  Type::Qualifiers tq1 = type1->get_qualifiers(), tq2 = type2->get_qualifiers();
  type1->get_qualifiers() = Type::Qualifiers();
  type2->get_qualifiers() = Type::Qualifiers();
  bool result;
#ifdef DEBUG
  std::cout << "unifyInexact type 1 is ";
  type1->print( std::cout );
  std::cout << "type 2 is ";
  type2->print( std::cout );
  std::cout << std::endl;
#endif
  if( !unifyExact( type1, type2, env, needAssertions, haveAssertions, openVars, widenMode, indexer ) ) {
#ifdef DEBUG
    std::cout << "unifyInexact: no exact unification found" << std::endl;
#endif
    if( ( common = commonType( type1, type2, widenMode.widenFirst, widenMode.widenSecond, indexer, env, openVars ) ) ) {
      common->get_qualifiers() = tq1 + tq2;
#ifdef DEBUG
      std::cout << "unifyInexact: common type is ";
      common->print( std::cout );
      std::cout << std::endl;
#endif
      result = true;
    } else {
#ifdef DEBUG
      std::cout << "unifyInexact: no common type found" << std::endl;
#endif
      result = false;
    }
  } else {
    if( tq1 != tq2 ) {
      if( ( tq1 > tq2 || widenMode.widenFirst ) && ( tq2 > tq1 || widenMode.widenSecond ) ) {
        common = type1->clone();
        common->get_qualifiers() = tq1 + tq2;
        result = true;
      } else {
        result = false;
      }
    } else {
      result = true;
    }
  }
  type1->get_qualifiers() = tq1;
  type2->get_qualifiers() = tq2;
  return result;
}

Unify::Unify( Type *type2, TypeEnvironment &env, AssertionSet &needAssertions, AssertionSet &haveAssertions, const OpenVarSet &openVars, WidenMode widenMode, const SymTab::Indexer &indexer )
  : result( false ), type2( type2 ), env( env ), needAssertions( needAssertions ), haveAssertions( haveAssertions ), openVars( openVars ), widenMode( widenMode ), indexer( indexer )
{
}

void 
Unify::visit(VoidType *voidType)
{
  result = dynamic_cast< VoidType* >( type2 );
}

void 
Unify::visit(BasicType *basicType)
{
  if( BasicType *otherBasic = dynamic_cast< BasicType* >( type2 ) ) {
    result = basicType->get_kind() == otherBasic->get_kind();
  }
}

void
markAssertionSet( AssertionSet &assertions, DeclarationWithType *assert )
{
///   std::cout << "assertion set is" << std::endl;
///   printAssertionSet( assertions, std::cout, 8 );
///   std::cout << "looking for ";
///   assert->print( std::cout );
///   std::cout << std::endl;
  AssertionSet::iterator i = assertions.find( assert );
  if( i != assertions.end() ) {
///     std::cout << "found it!" << std::endl;
    i->second = true;
  }
}

void
markAssertions( AssertionSet &assertion1, AssertionSet &assertion2, Type *type )
{
  for( std::list< TypeDecl* >::const_iterator tyvar = type->get_forall().begin(); tyvar != type->get_forall().end(); ++tyvar ) {
    for( std::list< DeclarationWithType* >::const_iterator assert = (*tyvar)->get_assertions().begin(); assert != (*tyvar)->get_assertions().end(); ++assert ) {
      markAssertionSet( assertion1, *assert );
      markAssertionSet( assertion2, *assert );
    }
  }
}

void 
Unify::visit(PointerType *pointerType)
{
  if( PointerType *otherPointer = dynamic_cast< PointerType* >( type2 ) ) {
    result = unifyExact( pointerType->get_base(), otherPointer->get_base(), env, needAssertions, haveAssertions, openVars, WidenMode( false, false ), indexer );
    markAssertions( haveAssertions, needAssertions, pointerType );
    markAssertions( haveAssertions, needAssertions, otherPointer );
  }
}

void 
Unify::visit(ArrayType *arrayType)
{
  // XXX -- compare array dimension
  ArrayType *otherArray = dynamic_cast< ArrayType* >( type2 );
  if( otherArray && arrayType->get_isVarLen() == otherArray->get_isVarLen() ) {
    result = unifyExact( arrayType->get_base(), otherArray->get_base(), env, needAssertions, haveAssertions, openVars, WidenMode( false, false ), indexer );
  }
}

template< typename Iterator1, typename Iterator2 >
bool
unifyDeclList( Iterator1 list1Begin, Iterator1 list1End, Iterator2 list2Begin, Iterator2 list2End, TypeEnvironment &env, AssertionSet &needAssertions, AssertionSet &haveAssertions, const OpenVarSet &openVars, const SymTab::Indexer &indexer ) {
  for( ; list1Begin != list1End && list2Begin != list2End; ++list1Begin, ++list2Begin ) {
    if( !unifyExact( (*list1Begin)->get_type(), (*list2Begin)->get_type(), env, needAssertions, haveAssertions, openVars, WidenMode( false, false ), indexer ) ) {
      return false;
    }
  }
  if( list1Begin != list1End || list2Begin != list2End ) {
    return false;
  } else {
    return true;
  }
}

void 
Unify::visit(FunctionType *functionType)
{
  FunctionType *otherFunction = dynamic_cast< FunctionType* >( type2 );
  if( otherFunction && functionType->get_isVarArgs() == otherFunction->get_isVarArgs() ) {
  
    if( unifyDeclList( functionType->get_parameters().begin(), functionType->get_parameters().end(), otherFunction->get_parameters().begin(), otherFunction->get_parameters().end(), env, needAssertions, haveAssertions, openVars, indexer ) ) {
    
      if( unifyDeclList( functionType->get_returnVals().begin(), functionType->get_returnVals().end(), otherFunction->get_returnVals().begin(), otherFunction->get_returnVals().end(), env, needAssertions, haveAssertions, openVars, indexer ) ) {

        markAssertions( haveAssertions, needAssertions, functionType );
        markAssertions( haveAssertions, needAssertions, otherFunction );

        result = true;
      }
    }
  }
}

template< typename RefType >
void
Unify::handleRefType( RefType *inst, Type *other )
{  
  RefType *otherStruct = dynamic_cast< RefType* >( other );
  result = otherStruct && inst->get_name() == otherStruct->get_name();
}  

void 
Unify::visit(StructInstType *structInst)
{
  handleRefType( structInst, type2 );
}

void 
Unify::visit(UnionInstType *unionInst)
{
  handleRefType( unionInst, type2 );
}

void 
Unify::visit(EnumInstType *enumInst)
{
  handleRefType( enumInst, type2 );
}

void 
Unify::visit(ContextInstType *contextInst)
{
  handleRefType( contextInst, type2 );
}

void 
Unify::visit(TypeInstType *typeInst)
{
  assert( openVars.find( typeInst->get_name() ) == openVars.end() );
  TypeInstType *otherInst = dynamic_cast< TypeInstType* >( type2 );
  if( otherInst && typeInst->get_name() == otherInst->get_name() ) {
    result = true;
///   } else {
///     NamedTypeDecl *nt = indexer.lookupType( typeInst->get_name() );
///     if( nt ) {
///       TypeDecl *type = dynamic_cast< TypeDecl* >( nt );
///       assert( type );
///       if( type->get_base() ) {
///         result = unifyExact( type->get_base(), typeInst, env, needAssertions, haveAssertions, openVars, WidenMode( false, false ), indexer );
///       }
///     }
  }
}

template< typename Iterator1, typename Iterator2 >
bool
unifyList( Iterator1 list1Begin, Iterator1 list1End, Iterator2 list2Begin, Iterator2 list2End, TypeEnvironment &env, AssertionSet &needAssertions, AssertionSet &haveAssertions, const OpenVarSet &openVars, WidenMode widenMode, const SymTab::Indexer &indexer ) {
  for( ; list1Begin != list1End && list2Begin != list2End; ++list1Begin, ++list2Begin ) {
    Type *commonType = 0;
    if( !unifyInexact( *list1Begin, *list2Begin, env, needAssertions, haveAssertions, openVars, widenMode, indexer, commonType ) ) {
      return false;
    }
    delete commonType;
  }
  if( list1Begin != list1End || list2Begin != list2End ) {
    return false;
  } else {
    return true;
  }
}

void 
Unify::visit(TupleType *tupleType)
{
  if( TupleType *otherTuple = dynamic_cast< TupleType* >( type2 ) ) {
    result = unifyList( tupleType->get_types().begin(), tupleType->get_types().end(), otherTuple->get_types().begin(), otherTuple->get_types().end(), env, needAssertions, haveAssertions, openVars, widenMode, indexer );
  }
}

} // namespace ResolvExpr