#ifndef EMPATHY_SEMA_UNI_CONTEXT_H
#define EMPATHY_SEMA_UNI_CONTEXT_H

namespace empathy::sema
{
    class UnificationRuleSet;

    class UnificationContext
    {
        public:
            static constexpr uint32_t InvalidIndex = numeric_limits< uint32_t >::max();

            UnificationContext( const ptr< UnificationRuleSet >& rules );
            UnificationContext( ptr< UnificationRuleSet >&& rules );

            const auto& rules() const { return m_rules; }

            uint32_t getLHSHoleIndex( const StringId& name ) const;
            uint32_t getRHSHoleIndex( const StringId& name ) const;

            uint32_t createValue();
            void setLHSHoleIndex( const StringId& name, uint32_t index );
            void setRHSHoleIndex( const StringId& name, uint32_t index );

            const optional< Term >& getValue( uint32_t index ) const
            {
                assert( m_values.size() > index );
                return m_values[index].first;
            }

            void setValue( uint32_t index, Term&& val, uint32_t complexity );

            UnificationContext& flip()
            {
                swap( m_currentLHSNamespaceIndex, m_currentRHSNamespaceIndex );
                return *this;
            }

            void incComplexity( uint32_t n = 1 ) { m_complexity += n; }

            uint32_t numUnknownValues() const { return m_numUnknownValues; }
            uint32_t complexity() const { return m_complexity; }
            auto score() const { return UnificationScore( m_complexity, m_pHoleDict->size() ); }

        private:
            ptr< UnificationRuleSet >                   m_rules;

            using StoredValue = pair< optional< Term >, uint32_t >;
            immer::vector< StoredValue >                m_values;

            uint32_t                                    m_currentLHSNamespaceIndex = 1;
            uint32_t                                    m_currentRHSNamespaceIndex = 2;

            uint32_t                                    m_numUnknownValues = 0;
            uint32_t                                    m_complexity = 0;

            using HoleName = pair< StringId, uint32_t >;
            using HoleDict = unordered_map< HoleName, uint32_t >;

            ptr< HoleDict >                             m_pHoleDict = make_shared< HoleDict >();
    };
}

#endif
