// Copyright (C) 2006, Ondra Kamenik

// $Id: static_atoms.h 1218 2007-03-19 21:52:49Z kamenik $

#ifndef OGP_STATIC_ATOMS
#define OGP_STATIC_ATOMS

#include "dynamic_atoms.h"

namespace ogp {

	class StaticAtoms : public Atoms, public Constants {
	protected:
		typedef map<const char*, int, ltstr> Tvarmap;
		typedef map<int, const char*> Tinvmap;
		/** Storage for names. */
		NameStorage varnames;
		/** Outer order of variables. */
		vector<const char*> varorder;
		/** This is the map mapping a variable name to the tree
		 * index. */
		Tvarmap vars;
		/** This is the inverse mapping. It maps a tree index to the
		 * variable name. */
		Tinvmap indices;
	public:
		StaticAtoms() : Atoms(), Constants(), varnames(), varorder(), vars()
			{}
		/* Copy constructor. */
		StaticAtoms(const StaticAtoms& a);
		/** Conversion from DynamicAtoms. This takes all atoms from
		 * the DynamicAtoms and adds its static version. The new tree
		 * indices are allocated in the passed OperationTree. Whole
		 * the process is traced in the map mapping old tree indices
		 * to new tree indices. */
		StaticAtoms(const DynamicAtoms& da, OperationTree& otree, Tintintmap& tmap)
			: Atoms(), Constants(), varnames(), varorder(), vars()
			{import_atoms(da, otree, tmap);}
		/* Destructor. */
		virtual ~StaticAtoms() {}
		/** This imports atoms from dynamic atoms inserting the new
		 * tree indices to the given tree (including constants). The
		 * mapping from old atoms to new atoms is traced in tmap. */
		void import_atoms(const DynamicAtoms& da, OperationTree& otree,
						  Tintintmap& tmap);
		/** If the name is constant, it returns its tree index if the
		 * constant is registered in Constants, it returns -1
		 * otherwise. If the name is not constant, it returns result
		 * from check_variable, which is implemented by a subclass. */
		int check(const char* name) const;
		/** This assigns a given tree index to the variable name. The
		 * name should have been checked before the call. */
		void assign(const char* name, int t);
		int nvar() const
			{return varnames.num();}
		/** This returns a vector of all variables. */
		vector<int> variables() const;
		/** This returns a tree index of the given variable. */
		int index(const char* name) const;
		/** This returns a name from the given tree index. NULL is
		 * returned if the tree index doesn't exist. */
		const char* inv_index(int t) const;
		/** This returns a name in a outer ordering. (There is no other ordering.) */
		const char* name(int i) const
			{return varorder[i];}
		/** Debug print. */
		void print() const;
		/** This registers a variable. A subclass can reimplement
		 * this, for example, to ensure uniqueness of the
		 * name. However, this method should be always called in
		 * overriding methods to do the registering job. */
		virtual void register_name(const char* name);
		/** Return the name storage to allow querying to other
		 * classes. */
		const NameStorage& get_name_storage() const
			{return varnames;}
	protected:
		/** This checks the variable. The implementing subclass might
		 * want to throw an exception if the variable has not been
		 * registered. */
		virtual int check_variable(const char* name) const = 0;
	};
};

#endif

// Local Variables:
// mode:C++
// End: