#include "builtins/builtins.h"

namespace empathy::builtins
{
    UniGen UnifyTDecl( const Term& lhs, const Term& rhs, UnificationContext& c )
    {
        auto tdecl = FromValue< TDecl >( *ValueFromIRExpr( lhs ) );
        assert( tdecl );

        // 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( tdecl->type(), tdecl->value(), c ) )
        {
            auto localC = c;
            localC.setRHSNamespaceIndex( savedRHSNamespaceIndex );
            co_yield Unify( u, rhs, localC );
        }
    }

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

        e.unificationRuleSet()->addHalfUnificationRule( tDeclPat,
            []( const Term& lhs, UnificationContext& c ) -> UniGen
            {
                auto tdecl = FromValue< TDecl >( *ValueFromIRExpr( lhs ) );
                assert( tdecl );

                // 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( tdecl->type(), tdecl->value(), c ) )
                {
                    auto localC = c;
                    localC.setRHSNamespaceIndex( savedRHSNamespaceIndex );
                    co_yield { u, localC };
                }
            } );

        e.unificationRuleSet()->addSymRule( tDeclPat, ANYTERM( _ ), UnifyTDecl );
        e.unificationRuleSet()->addSymRule( tDeclPat, UnifyTDecl );
    }
}
