52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
|
// Indicates whether we are in trhe second unification pass
bool secondPass() const { return m_secondPass; }
void setSecondPass() { m_secondPass = true; }
const optional< Term >& getValue( uint32_t index ) const
{
assert( m_values.size() > index );
return m_values[index].m_term;
}
template< typename T >
void setValue( uint32_t index, T&& val )
{
assert( m_values.size() > index );
if( m_values[index].m_required && !m_values[index].m_term )
--m_numUnknownValues;
if( m_values[index].m_term )
m_complexity -= GetComplexity( *m_values[index].m_term );
m_values = m_values.set( index, { forward< T >( val ), true } );
m_complexity += GetComplexity( *m_values[index].m_term );
}
UnificationContext& flip()
{
swap( m_currentLHSNamespaceIndex, m_currentRHSNamespaceIndex );
return *this;
}
|
|
|
|
|
|
|
|
|
|
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
|
// Indicates whether we are in trhe second unification pass
bool secondPass() const { return m_secondPass; }
void setSecondPass() { m_secondPass = true; }
const optional< Term >& getValue( uint32_t index ) const
{
assert( m_pCow->values.size() > index );
return m_pCow->values[index].m_term;
}
template< typename T >
void setValue( uint32_t index, T&& val )
{
assert( m_pCow->values.size() > index );
if( m_pCow->values[index].m_required && !m_pCow->values[index].m_term )
--m_numUnknownValues;
if( m_pCow->values[index].m_term )
m_complexity -= GetComplexity( *m_pCow->values[index].m_term );
CoW( m_pCow )->values[index] = { forward< T >( val ), true };
m_complexity += GetComplexity( *m_pCow->values[index].m_term );
}
UnificationContext& flip()
{
swap( m_currentLHSNamespaceIndex, m_currentRHSNamespaceIndex );
return *this;
}
|
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
|
struct StoredValue
{
optional< Term > m_term;
bool m_required = false;
};
immer::vector< StoredValue > m_values;
unordered_set< uint32_t > lockedHoles;
};
ptr< Cow > m_pCow = make_shared< Cow >();
bool m_valuesAreRequired = true;
bool m_secondPass = false;
};
}
#endif
|
<
<
>
|
|
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
|
struct StoredValue
{
optional< Term > m_term;
bool m_required = false;
};
uint32_t m_currentLHSNamespaceIndex = 1;
uint32_t m_currentRHSNamespaceIndex = 2;
uint32_t m_nextNamespaceIndex = 3;
uint32_t m_numUnknownValues = 0;
uint32_t m_complexity = 0;
uint32_t m_numAnonymousHoles = 0;
using HoleName = pair< StringId, uint32_t >;
struct Cow
{
vector< StoredValue > values;
unordered_map< HoleName, uint32_t > holeDict;
unordered_set< uint32_t > lockedHoles;
};
ptr< Cow > m_pCow = make_shared< Cow >();
bool m_valuesAreRequired = true;
bool m_secondPass = false;
};
}
#endif
|