Goose  Artifact [6d6bf33752]

Artifact 6d6bf3375298627b8443734036135bfff39c26558fa0d43ab21dd1a271d9ddd9:

• File bs/sema/substitute.cpp — part of check-in [43e22af793] at 2019-08-05 02:45:01 on branch trunk —
  • Unification now works in two passes. The second pass gives unification rules a chance to match again after all the holes have been resolved and substituted.
  • Fixed many horrible bugs in various unification rules that managed to go by unnoticed until the above change, after which they made everything catch on fire.
  • Simplified the ct_int and ct_string unification rules to take advantage of the new unification behavior. Everything finally works as intended wrt to ct_int versus RT integers.
  • Removed unification callbacks. It was a system to provide a way to perform unification work post hole substitution, so it is now obsolete.
  (user: achavasse size: 2709)

#include "sema.h"

namespace empathy::sema
{
    Term Substitute( const Term& src, const UnificationContext& context )
    {
        if( !holds_alternative< pvec >( src.content() ) )
            return src;

        if( auto optHole = HoleFromIRExpr( src ) )
        {
            const auto& hole = *optHole;

            // We only substitute indexed holes. If we encounter a named hole,
            // output it as is.
            if( !holds_alternative< uint32_t >( hole ) )
                return src;

            const auto& optVal = context.getValue( get< uint32_t >( hole ) );
            if( !optVal )
                return MkHole( "_"_sid );

            return Substitute( *optVal, context );
        }

        const auto& vec = *get< pvec >( src.content() );
        immer::vector< Term > outputTerms;
        auto vt = outputTerms.transient();
        bool faulty = false;

        for( auto&& t : vec.terms() )
        {
            auto newT = Substitute( t, context );
              faulty = faulty || newT.isFaulty();
            vt.push_back( move( newT ) );
        }

        return Term( src.location(), make_shared< Vector >( vt.persistent(), faulty ) );
    }

    Term SubstituteNamed( const Term& src, const UnificationContext& context )
    {
        if( !holds_alternative< pvec >( src.content() ) )
            return src;

        if( auto optHole = HoleFromIRExpr( src ) )
        {
            const auto& hole = *optHole;

            if( holds_alternative< StringId >( hole ) )
            {
                // If the name is not found, output it as is.
                auto index = context.getLHSHoleIndex( get< StringId >( hole ) );
                if( index == UnificationContext::InvalidIndex )
                    return src;

                const auto& val = context.getValue( index );
                if( !val )
                    return src;

                return SubstituteNamed( *val, context );
            }
            else
            {
                const auto& optVal = context.getValue( get< uint32_t >( hole ) );
                if( !optVal )
                    return MkHole( "_"_sid );

                return SubstituteNamed( *optVal, context );
            }
        }

        const auto& vec = *get< pvec >( src.content() );
        immer::vector< Term > outputTerms;
        auto vt = outputTerms.transient();
        bool faulty = false;

        for( auto&& t : vec.terms() )
        {
            auto newT = SubstituteNamed( t, context );
            faulty = faulty || newT.isFaulty();
            vt.push_back( move( newT ) );
        }

        return Term( src.location(), make_shared< Vector >( vt.persistent(), faulty ) );
    }
}