Goose  Artifact [f135278fd3]

Artifact f135278fd39a2d58d9b3330721fb2a8bc6c16a866f856e5c09a7b349945fa412:

• File bs/sema/uni-3way.cpp — part of check-in [0e66d22527] at 2019-03-30 15:30:31 on branch trunk —
  • Changed type's type representation to be able to pass types around as value anywhere.
  • Fixed a bunch of bugs.
  (user: achavasse size: 2531)

#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( _ ), ANYTERM( _ ) ),
            []( 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 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 ) )
                {
                    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 );
    }
}