Goose  Artifact [c6fcecb859]

Artifact c6fcecb859bf00a25d184b31632b4ed4e088a1def020c112724cd77e27d0edc1:

  • File bs/sema/uni-basicrules.cpp — part of check-in [403ca496c8] at 2019-03-10 19:20:48 on branch trunk — Overloading: first untested draft of utrie unification. (user: achavasse size: 4315)

#include "sema.h"

namespace empathy::sema
{
    UniGen HalfUnifyVectors( const Vector::container_type< Term >& lTerms, size_t i, const Vector& solutionVec, UnificationContext& c )
    {
        assert( i < lTerms.size() );

        auto localC = c;

        for( auto&& [u,c] : HalfUnify( lTerms[i], localC ) )
        {
            auto vec = Vector::MakeAppend( solutionVec, move( u ) );

            if( i == ( lTerms.size() - 1 ) )
                co_yield { TERM( make_shared< Vector >( move( vec ) ) ), c };
            else
                co_yield HalfUnifyVectors( lTerms, i + 1, vec, c );
        }
    }

    UniGen UnifyVectors( const Vector::container_type< Term >& lTerms, const Vector::container_type< Term >& rTerms, size_t i, const Vector& solutionVec, UnificationContext& c )
    {
        assert( lTerms.size() == rTerms.size() );
        assert( i < lTerms.size() );

        auto localC = c;

        for( auto&& [u,c] : Unify( lTerms[i], rTerms[i], localC ) )
        {
            auto vec = Vector::MakeAppend( solutionVec, move( u ) );

            if( i == ( lTerms.size() - 1 ) )
                co_yield { TERM( make_shared< Vector >( move( vec ) ) ), c };
            else
                co_yield UnifyVectors( lTerms, rTerms, i + 1, vec, c );
        }
    }

    void SetupBasicUnificationRules( UnificationRuleSet& ruleSet )
    {
        // Default half-unification rule
        ruleSet.addHalfUnificationRule( ANYTERM( T ), []( const Term& lhs, UnificationContext& c ) -> UniGen
        {
            // NOTE: the score here is always 0 because:
            // Vectors are going to fall into the vector half-unification rule below,
            // and holes are going to have their own rules. So we only are here for terminal expressions.
            co_yield { lhs, c };
        } );

        // Identity unification rule
        ruleSet.addSymRule( ANYTERM( T ), []( const Term& lhs, const Term& rhs, UnificationContext& c ) -> UniGen
        {
            assert( lhs == rhs );

            // NOTE: the score here is always 0 because:
            // Vectors of identical size are going to fall into the vector unification rule below,
            // and holes are going to have their own rules. So we only are here for literal matches
            // of terminal expressions.
            co_yield { lhs, c };
        } );

        // Half-Unification rule for vectors:
        // They are recursed into and each contained members are half-unified.
        // Note: the repetition term, if any, is ignored. The repetition term is only for vector patterns
        // for now. We'll have to see how to handle variadic functions later.
        ruleSet.addHalfUnificationRule( VECOFLENGTH( VL ), []( const Term& lhs, UnificationContext& c ) -> UniGen
        {
            assert( holds_alternative< pvec >( lhs.content() ) );

            c.incComplexity();

            const auto& lVector = get< pvec >( lhs.content() );
            const auto& lTerms = lVector->terms();

            if( lTerms.empty() )
            {
                co_yield { lhs, c };
                co_return;
            }

            Vector sol;
            co_yield HalfUnifyVectors( lTerms, 0, sol, c );
        } );

        // Unification rule for vectors of identical length:
        // They are recursed into and each contained members are unified.
        // Note: the repetition term, if any, is ignored. The repetition term is only for vector patterns
        // for now. We'll have to see how to handle variadic functions later.
        ruleSet.addSymRule( VECOFLENGTH( VL ), []( const Term& lhs, const Term& rhs, UnificationContext& c ) -> UniGen
        {
            assert( holds_alternative< pvec >( lhs.content() ) );
            assert( holds_alternative< pvec >( rhs.content() ) );

            c.incComplexity( 2 );

            const auto& lVector = get< pvec >( lhs.content() );
            const auto& rVector = get< pvec >( rhs.content() );

            const auto& lTerms = lVector->terms();
            const auto& rTerms = rVector->terms();

            if( lTerms.empty() )
            {
                co_yield { lhs, c };
                co_return;
            }

            Vector sol;
            co_yield UnifyVectors( lTerms, rTerms, 0, sol, c );
        } );
    }
}