#include "sema.h"
namespace empathy::sema
{
UniGen HalfUnifyVectors( const Vector::container_type< Term >& lTerms, size_t i, const Vector& solutionVec, UnificationContext& c )
{
assert( i < lTerms.size() );
auto localC = c;
for( auto&& [u,c] : HalfUnify( lTerms[i], localC ) )
{
auto vec = Vector::MakeAppend( solutionVec, move( u ) );
if( i == ( lTerms.size() - 1 ) )
co_yield { TERM( make_shared< Vector >( move( vec ) ) ), c };
else
co_yield HalfUnifyVectors( lTerms, i + 1, vec, c );
}
}
UniGen UnifyVectors( const Vector::container_type< Term >& lTerms, const Vector::container_type< Term >& rTerms, size_t i, const Vector& solutionVec, UnificationContext& c )
{
assert( lTerms.size() == rTerms.size() );
assert( i < lTerms.size() );
auto localC = c;
for( auto&& [u,c] : Unify( lTerms[i], rTerms[i], localC ) )
{
auto vec = Vector::MakeAppend( solutionVec, move( u ) );
if( i == ( lTerms.size() - 1 ) )
co_yield { TERM( make_shared< Vector >( move( vec ) ) ), c };
else
co_yield UnifyVectors( lTerms, rTerms, i + 1, vec, c );
}
}
void SetupBasicUnificationRules( UnificationRuleSet& ruleSet )
{
// Default half-unification rule
ruleSet.addHalfUnificationRule( ANYTERM( T ), []( const Term& lhs, UnificationContext& c ) -> UniGen
{
// NOTE: the score here is always 0 because:
// Vectors are going to fall into the vector half-unification rule below,
// and holes are going to have their own rules. So we only are here for terminal expressions.
co_yield { lhs, c };
} );
// Identity unification rule
ruleSet.addSymRule( ANYTERM( T ), []( const Term& lhs, const Term& rhs, UnificationContext& c ) -> UniGen
{
assert( lhs == rhs );
// NOTE: the score here is always 0 because:
// Vectors of identical size are going to fall into the vector unification rule below,
// and holes are going to have their own rules. So we only are here for literal matches
// of terminal expressions.
co_yield { lhs, c };
} );
// Half-Unification rule for vectors:
// They are recursed into and each contained members are half-unified.
// Note: the repetition term, if any, is ignored. The repetition term is only for vector patterns
// for now. We'll have to see how to handle variadic functions later.
ruleSet.addHalfUnificationRule( VECOFLENGTH( VL ), []( const Term& lhs, UnificationContext& c ) -> UniGen
{
assert( holds_alternative< pvec >( lhs.content() ) );
c.incComplexity();
const auto& lVector = get< pvec >( lhs.content() );
const auto& lTerms = lVector->terms();
if( lTerms.empty() )
{
co_yield { lhs, c };
co_return;
}
Vector sol;
co_yield HalfUnifyVectors( lTerms, 0, sol, c );
} );
// Unification rule for vectors of identical length:
// They are recursed into and each contained members are unified.
// Note: the repetition term, if any, is ignored. The repetition term is only for vector patterns
// for now. We'll have to see how to handle variadic functions later.
ruleSet.addSymRule( VECOFLENGTH( VL ), []( const Term& lhs, const Term& rhs, UnificationContext& c ) -> UniGen
{
assert( holds_alternative< pvec >( lhs.content() ) );
assert( holds_alternative< pvec >( rhs.content() ) );
c.incComplexity( 2 );
const auto& lVector = get< pvec >( lhs.content() );
const auto& rVector = get< pvec >( rhs.content() );
const auto& lTerms = lVector->terms();
const auto& rTerms = rVector->terms();
if( lTerms.empty() )
{
co_yield { lhs, c };
co_return;
}
Vector sol;
co_yield UnifyVectors( lTerms, rTerms, 0, sol, c );
} );
}
}