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

#ifndef RESOLVEXPR_TYPEENVIRONMENT_H
#define RESOLVEXPR_TYPEENVIRONMENT_H

#include <string>
#include <set>
#include <list>
#include <iostream>

#include "SynTree/SynTree.h"
#include "SynTree/Type.h"
#include "SynTree/TypeSubstitution.h"
#include "SynTree/Declaration.h"

namespace ResolvExpr {

typedef std::map< DeclarationWithType*, bool > AssertionSet;
typedef std::map< std::string, TypeDecl::Kind > OpenVarSet;

void printAssertionSet( const AssertionSet &, std::ostream &, int indent = 0 );
void printOpenVarSet( const OpenVarSet &, std::ostream &, int indent = 0 );

struct EqvClass
{
  std::set< std::string > vars;
  Type *type;
  bool allowWidening;
  TypeDecl::Kind kind;
  
  void initialize( const EqvClass &src, EqvClass &dest );
  EqvClass();
  EqvClass( const EqvClass &other );
  EqvClass &operator=( const EqvClass &other );
  ~EqvClass();
  void print( std::ostream &os, int indent = 0 ) const;
};

class TypeEnvironment
{
public:
  bool lookup( const std::string &var, EqvClass &eqvClass ) const;
  void add( const EqvClass &eqvClass );
  void add( const std::list< TypeDecl* > &tyDecls );
  template< typename SynTreeClass > int apply( SynTreeClass *&type ) const;
  template< typename SynTreeClass > int applyFree( SynTreeClass *&type ) const;
  void makeSubstitution( TypeSubstitution &result ) const;
  bool isEmpty() const { return env.empty(); }
  void print( std::ostream &os, int indent = 0 ) const;
  void combine( const TypeEnvironment &second, Type *(*combineFunc)( Type*, Type* ) );
  void simpleCombine( const TypeEnvironment &second );
  void extractOpenVars( OpenVarSet &openVars ) const;
  TypeEnvironment *clone() const { return new TypeEnvironment( *this ); }
  
  typedef std::list< EqvClass >::iterator iterator;
  iterator begin() { return env.begin(); }
  iterator end() { return env.end(); }
  typedef std::list< EqvClass >::const_iterator const_iterator;
  const_iterator begin() const { return env.begin(); }
  const_iterator end() const { return env.end(); }
private:
  std::list< EqvClass > env;
  
  std::list< EqvClass >::iterator internal_lookup( const std::string &var );
};

template< typename SynTreeClass >
int 
TypeEnvironment::apply( SynTreeClass *&type ) const
{
  TypeSubstitution sub;
  makeSubstitution( sub );
  return sub.apply( type );
}

template< typename SynTreeClass >
int 
TypeEnvironment::applyFree( SynTreeClass *&type ) const
{
  TypeSubstitution sub;
  makeSubstitution( sub );
  return sub.applyFree( type );
}

} // namespace ResolvExpr

#endif /* #ifndef RESOLVEXPR_TYPEENVIRONMENT_H */