Goose  Artifact [d3e5a7db5f]

Artifact d3e5a7db5fdd96634d9ea59ead8295676d1a88c9cbb58053a8ad86e2ce86e752:

• File bs/sema/uni-3way.cpp — part of check-in [61b4955ba0] at 2019-03-23 14:04:07 on branch trunk — ir: made it possible to use anonymous ANYTERM patterns in matching. (user: achavasse size: 2524)

#include "sema.h"

namespace empathy::sema
{
    Term Mk3WayUnificationTerm( const Term& term1, const Term& term2 )
    {
        return TVEC( TSID( uni ), term1, term2 );
    }

    UniGen Unify3Way( const Term& lhs, const Term& rhs, UnificationContext& c )
    {
        auto result = Decompose( lhs,
            Vec(
                Lit( "uni"_sid ),
                SubTerm(),
                SubTerm()
            )
        );

        assert( result );
        auto&& [t1,t2] = *result;

        // Both of the expressions are side by side in the same input expresion, which
        // means their hole names share the same namespace. So pretend that both the LHS and RHS
        // namespaces are the same for their unification, but restore it after.
        auto savedRHSNamespaceIndex = c.RHSNamespaceIndex();
        c.setRHSNamespaceIndex( c.LHSNamespaceIndex() );

        for( auto&& [u,c] : Unify( t1, t2, c ) )
        {
            auto localC = c;
            localC.setRHSNamespaceIndex( savedRHSNamespaceIndex );
            co_yield Unify( u, rhs, localC );
        }
    }

    void Setup3WayUnificationRules( UnificationRuleSet& ruleSet )
    {
        ruleSet.addHalfUnificationRule( TVEC( TSID( _ ), ANYTERM( _ ), ANYTERM( _ ) ),
            []( const Term& lhs, UnificationContext& c ) -> UniGen
            {
                auto result = Decompose( lhs,
                    Vec(
                        Lit( "uni"_sid ),
                        SubTerm(),
                        SubTerm()
                    )
                );

                assert( result );
                auto&& [t1,t2] = *result;

                // Both of the expressions are side by side in the same input expresion, which
                // means their hole names share the same namespace. So pretend that both the LHS and RHS
                // namespaces are the same for their unification, but restore it after.
                auto savedRHSNamespaceIndex = c.RHSNamespaceIndex();
                c.setRHSNamespaceIndex( c.LHSNamespaceIndex() );

                for( auto&& [u,c] : Unify( t1, t2, c ) )
                {
                    auto localC = c;
                    localC.setRHSNamespaceIndex( savedRHSNamespaceIndex );
                    co_yield { u, localC };
                }
            } );

        ruleSet.addSymRule( TVEC( TSID( _ ), ANYTERM( _ ), ANYTERM( _ ) ), ANYTERM( _ ), Unify3Way );
        ruleSet.addSymRule( TVEC( TSID( _ ), ANYTERM( _ ), ANYTERM( _ ) ), Unify3Way );
    }
}