#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 );
}
}