#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