//
// Cforall Version 1.0.0 Copyright (C) 2015 University of Waterloo
//
// The contents of this file are covered under the licence agreement in the
// file "LICENCE" distributed with Cforall.
//
// TypeEnvironment.h --
//
// Author           : Richard C. Bilson
// Created On       : Sun May 17 12:24:58 2015
// Last Modified By : Peter A. Buhr
// Last Modified On : Sun May 17 12:26:52 2015
// Update Count     : 2
//

#ifndef TYPEENVIRONMENT_H
#define 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 {
	struct AssertCompare {
		bool operator()( DeclarationWithType * d1, DeclarationWithType * d2 ) const;
	};
	typedef std::map< DeclarationWithType*, bool, AssertCompare > AssertionSet;
	typedef std::map< std::string, TypeDecl::Data > 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::Data data;

		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 Type::ForallList &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 // TYPEENVIRONMENT_H */

// Local Variables: //
// tab-width: 4 //
// mode: c++ //
// compile-command: "make install" //
// End: //