Goose  Diff

#include "sema.h"
#include "builtins/builtins.h"

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

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

        assert( result );
        auto tdecl = FromValue< TDecl >( *ValueFromIRExpr( lhs ) );
        assert( tdecl );
        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 ) )
        for( auto&& [u,c] : Unify( tdecl->type(), tdecl->value(), c ) )
        {
            auto localC = c;
            localC.setRHSNamespaceIndex( savedRHSNamespaceIndex );
            co_yield Unify( u, rhs, localC );
        }
    }

    void Setup3WayUnificationRules( UnificationRuleSet& ruleSet )
    void SetupTDeclUnification( Env& e )
    {
        auto tDeclPat = ValueToIRExpr( Value( GetValueType< TDecl >(), TVEC( ANYTERM( _ ), ANYTERM( _ ) ) ) );

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

                assert( result );
                auto tdecl = FromValue< TDecl >( *ValueFromIRExpr( lhs ) );
                assert( tdecl );
                auto&& [t1,t2] = *result;

                // Both of the expressions are side by side in the same input expression, 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 ) )
                for( auto&& [u,c] : Unify( tdecl->type(), tdecl->value(), c ) )
                {
                    auto localC = c;
                    localC.setRHSNamespaceIndex( savedRHSNamespaceIndex );
                    co_yield { u, localC };
                }
            } );

        ruleSet.addSymRule( TVEC( TSID( uni ), ANYTERM( _ ), ANYTERM( _ ) ), ANYTERM( _ ), Unify3Way );
        ruleSet.addSymRule( TVEC( TSID( uni ), ANYTERM( _ ), ANYTERM( _ ) ), Unify3Way );
        e.unificationRuleSet()->addSymRule( tDeclPat, ANYTERM( _ ), UnifyTDecl );
        e.unificationRuleSet()->addSymRule( tDeclPat, UnifyTDecl );
    }
}