#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( uni ), ANYTERM( t1 ), ANYTERM( t1 ) ),
            []( 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( uni ), ANYTERM( t1 ), ANYTERM( t2 ) ), ANYTERM( rhs ), Unify3Way );
        ruleSet.addSymRule( TVEC( TSID( uni ), ANYTERM( t1 ), ANYTERM( t2 ) ), Unify3Way );
    }
}
