Goose  Artifact [3d3a0385b4]

Artifact 3d3a0385b41c970f8ca236bb66664a02804c1714bc78ca3c634d753ac728cfcc:

• File bs/sema/uni-context.h — part of check-in [06b4cded56] at 2019-03-25 22:39:47 on branch trunk — Higher order functions: it is now possible to bind a template lambda to a function typed parameter. (user: achavasse size: 3549)

#ifndef EMPATHY_SEMA_UNI_CONTEXT_H
#define EMPATHY_SEMA_UNI_CONTEXT_H

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

            UnificationContext( const Context& c );
            UnificationContext( Context&& c );

            const auto& context() const { return m_context; }
            const auto& env() const { return m_context.env(); }
            const auto& rules() const { return env()->unificationRuleSet(); }

            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 );

            void eraseLHSName( const StringId& name );
            void eraseRHSName( const StringId& name );

            uint32_t LHSNamespaceIndex() const { return m_currentLHSNamespaceIndex; }
            uint32_t RHSNamespaceIndex() const { return m_currentRHSNamespaceIndex; }

            void setLHSNamespaceIndex( uint32_t index ) { m_currentLHSNamespaceIndex = index; }
            void setRHSNamespaceIndex( uint32_t index ) { m_currentRHSNamespaceIndex = index; }

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

            template< typename T >
            void setValue( uint32_t index, T&& val, uint32_t complexity )
            {
                assert( m_values.size() > index );

                if( !m_values[index].first )
                    --m_numUnknownValues;

                m_complexity -= m_values[index].second;
                m_values = m_values.set( index, { forward< T >( val ), 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_pCow->holeDict.size() ); }

            // Used to detect and reject recursive hole nesting.
            bool isHoleLocked( uint32_t index ) const;
            void lockHole( uint32_t index );
            void unlockHole( uint32_t index );

        private:
            Context                                     m_context;

            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 >;

            struct Cow
            {
                unordered_map< HoleName, uint32_t > holeDict;
                unordered_set< uint32_t > lockedHoles;
            };

            ptr< Cow >                                  m_pCow = make_shared< Cow >();
    };
}

#endif