Goose  Check-in [3bf30e74ac]

        // ct_int type against a IntegerType type:
        // return the IntegerType type. We don't care if the
        // ct_int fits at this point, this will be dealt with by
        // the ct_int value type checking rule below.
        e.typeCheckingRuleSet()->addUnificationRule( TCRINFOS,
            ValueToEIR( rtIntTypePattern ),
            GetValueType< BigInt >(),
        []( const Term& lhs, const Term& rhs, const TypeCheckingContext& c ) -> TCGen
        {
            return HalfUnify( lhs, c );

        } );

        // Reject the ct_int param and IntegerType arg pattern,
        // so that it doesn't fall into the rule above which would be incorrect
        // in that case.
        e.typeCheckingRuleSet()->addTypeCheckingRule( TCRINFOS,

                ANYTERM( _ ) ) ),

            ValueToEIR( ValuePattern(
                TSID( constant ),
                GetValueType< BigInt >(),
                ANYTERM( _ ) ) ),

        []( const Term& lhs, const Term& rhs, const TypeCheckingContext& tcc ) -> TCGen
        {
            // The rhs might not be constant. It can happen even with ct_int if the rhs is a
            // fake argument pattern generated to unify a higher-order function param.
            // It means that we are unifying a function parameter against any ct_int value,
            // which we can't (because we have to know the value to safely convert it),
            // so we reject it.
            auto rhsVal = *ValueFromEIR( rhs );
            if( !rhsVal.isConstant() )
                co_return;

            auto lhsVal = ValuePatternFromIRExpr( lhs );
            if( !lhsVal )
                co_return;

            for( auto&& [s,tcc] : HalfUnify( lhsVal->type(), tcc ) )


            {
                // We need to defer the calculation of the init value until after the rest of the type checking is complete,
                // because we need to make sure that any hole present in the integer type is resolved before we can do
                // the sign/bitsize check. However, since we still need to be able to manipulate the result as a value in
                // the mean time, we construct a value with the correct (but possibly not complete yet type), and a payload
                // that contains the type + the ct_int value wrapped with a post process callback that finalizes the job.
                auto wrapped = WrapWithPostprocFunc( VEC( lhsVal->type(), rhs ),
                []( const Term& t, TypeCheckingContext tcc ) -> optional< Term >
                {
                    auto result = Decompose( t,
                        Vec(
                            SubTerm(),
                            SubTerm()
                        )
                    );

                    assert( result );
                    auto&& [type, rhs] = *result;

                    auto ct = *FromValue< BigInt >( *ValueFromEIR( rhs ) );

                    auto rttypeVal = ValueFromEIR( type );
                    assert( rttypeVal );

                    auto rttype = FromValue< IntegerType >( *rttypeVal );
                    assert( rttype );

                    APSInt valToLoad;

                    if( rttype->m_signed )
                    {
                        if( ct.getMinSignedBits() > rttype->m_numBits )
                            return nullopt;

                        valToLoad = ct.sext( rttype->m_numBits );
                        valToLoad.setIsSigned( true );
                    }
                    else
                    {
                        if( ct.isNegative() )
                            return nullopt;

                        if( ct.getActiveBits() > rttype->m_numBits )
                            return nullopt;

                        valToLoad = ct.zext( rttype->m_numBits );
                        valToLoad.setIsSigned( false );
                    }

                    return TERM( valToLoad );
                } );

                co_yield { ValueToEIR( Value( s, move( wrapped ) ) ), tcc };
            }
        } );

        auto rtInt8TypePattern = Value( TypeType(), MkStdType( TSID( integer ),
            VEC( TERM( 8U ), ANYTERM( _ ) ) ) );

        auto rtInt8PtrTypePattern = Value( TypeType(), MkStdType( TSID( pointer ),
            ValueToEIR( rtInt8TypePattern ) ) );

        // ct_string type against a char*:
        // return the char* type.
        e.typeCheckingRuleSet()->addUnificationRule( TCRINFOS,
            ValueToEIR( rtInt8PtrTypePattern ),
            GetValueType< string >(),
        []( const Term& lhs, const Term& rhs, const TypeCheckingContext& c ) -> TCGen
        {
            co_yield HalfUnify( lhs, c );

        } );

        // ct_string constant type checking against a pointer to a integer( 8 ):
        // Emit a LoadConstantStr cir instruction.
        e.typeCheckingRuleSet()->addTypeCheckingRule( TCRINFOS,

            ValueToEIR( ValuePattern(

    }

    void SetupTDeclTypeChecking( Env& e )
    {
        auto tDeclPat = ValueToEIR( Value( GetValueType< TDecl >(), VEC( ANYTERM( _ ), ANYTERM( _ ) ) ) );

        e.typeCheckingRuleSet()->addHalfUnificationRule( TCRINFOS, tDeclPat,
            []( const Term& lhs, const TypeCheckingContext& c ) -> TCGen
            {
                auto tdecl = FromValue< TDecl >( *ValueFromEIR( lhs ) );
                assert( tdecl );
                return HalfUnify( tdecl->type(), c );
            } );

        e.typeCheckingRuleSet()->addTypeCheckingRule( TCRINFOS, tDeclPat, ANYTERM( _ ), UnifyTDecl );

    #define TCRINFOS TCRuleInfo{}
#endif

    class TypeCheckingRuleSet
    {
        public:
            using UniFunc = function< TCGen ( const Term& lhs, const Term& rhs, const TypeCheckingContext& ) >;
            using HalfUniFunc = function< TCGen ( const Term& lhs, const TypeCheckingContext& ) >;

            struct UniRule
            {
                UniFunc func;
                TCRuleInfo infos;
            };

            for( auto&& [t, payload] : Enumerate( get< 0 >( branch )->m_trie ) )
            {
                auto newC = tcc;
                newC.addComplexity( GetComplexity( t ) );

                auto lvec = Vector::MakeAppend( lhsVec, t );

                for( auto&& [s, tcc] : sema::HalfUnify( t, newC ) )
                    co_yield HalfUnify< T >( lvec, Vector::MakeAppend( solutionVec, move( s ) ), payload, tcc );
            }
        }
        else
            co_yield { lhsVec, solutionVec, *any_cast< T >( &get< 1 >( branch ) ), tcc };
    }

    template< typename U >

            for( auto&& [lv, sol, pRptNode, tcc] : HalfUnify< rpt_node >( lhs, sol, branch, tcc ) )
            {
                for( auto&& [rt, payload] : Enumerate( pRptNode->m_repetition ) )
                {
                    auto newC = tcc;
                    newC.addComplexity( GetComplexity( rt ) );

                    for( auto&& [s, c] : sema::HalfUnify( rt, newC ) )
                    {
                        auto localLhsVec = lv;
                        localLhsVec.setRepetitionTerm( rt );

                        auto localSol = sol;
                        localSol.setRepetitionTerm( move( s ) );
                        co_yield { localLhsVec, localSol, payload, c };
                    }
                }
            }
        }
    }
}

#endif

        if( !bestRule )
            co_return;

        co_yield bestRule->func( lhs, rhs, context );
    }

    TCGen HalfUnify( const Term& lhs, const TypeCheckingContext& context )
    {
        const auto& rules = context.rules()->halfUniRules();

        MatchSolution bestSol;
        optional< TypeCheckingRuleSet::HalfUniRule > bestRule;
        bool ambiguous = false;

        }

        // Let's not really worry about how to properly report this for now.
        if( ambiguous )
            throw runtime_error( "ambiguous half-unification rule" );

        if( !bestRule )
            co_return;

        co_yield bestRule->func( lhs, context );
    }
}

    TypeCheckingSolution FindBestTyping( const Term& lhs, const Term& rhs, const Context& context );

    using TCGen = Generator< pair< Term, TypeCheckingContext > >;

    TCGen TypeCheck( const Term& lhs, const Term& rhs, const TypeCheckingContext& context );

    TCGen Unify( const Term& lhs, const Term& rhs, const TypeCheckingContext& context );
    TCGen HalfUnify( const Term& lhs, const TypeCheckingContext& context );
}

#endif

#include "sema.h"

namespace goose::sema
{
    TCGen HalfUnifyVectors( const Vector::container_type< Term >& lTerms, size_t i, const Vector& solutionVec, TypeCheckingContext tcc )
    {
        assert( i < lTerms.size() );

        for( auto&& [u,tcc] : HalfUnify( lTerms[i], tcc ) )
        {
            auto vec = Vector::MakeAppend( solutionVec, move( u ) );

            if( i == ( lTerms.size() - 1 ) )
                co_yield { TERM( make_shared< Vector >( move( vec ) ) ), tcc };
            else
                co_yield HalfUnifyVectors( lTerms, i + 1, vec, tcc );
        }
    }

    TCGen UnifyVectors( const Vector::container_type< Term >& lTerms, const Vector::container_type< Term >& rTerms, size_t i,
        const Vector& solutionVec, TypeCheckingContext tcc )
    {
        assert( lTerms.size() == rTerms.size() );
        assert( i < lTerms.size() );

        for( auto&& [u,tcc] : Unify( lTerms[i], rTerms[i], tcc ) )

                co_yield TypeCheckVectors( lTerms, rTerms, i + 1, vec, tcc );
        }
    }

    void SetupBasicUnificationRules( TypeCheckingRuleSet& ruleSet )
    {
        // Default half-unification rule
        ruleSet.addHalfUnificationRule( TCRINFOS, ANYTERM( _ ), []( const Term& lhs, const TypeCheckingContext& tcc ) -> TCGen
        {
            // 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, tcc };
        } );

        // Identity unification rule
        ruleSet.addUnificationRule( TCRINFOS, ANYTERM( T ), []( const Term& lhs, const Term& rhs, const TypeCheckingContext& tcc ) -> TCGen
        {
            assert( lhs == rhs );

            // in the end if necessary.
            auto lpv = get< void* >( lhs );
            auto rpv = get< void* >( rhs );
            auto result = lpv == rpv ? lpv : nullptr;
            co_yield { result, tcc };
        } );

        // 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( TCRINFOS, VECOFLENGTH( _ ), []( const Term& lhs, const TypeCheckingContext& tcc ) -> TCGen

        {
            assert( holds_alternative< pvec >( lhs ) );

            const auto& lVector = get< pvec >( lhs );
            const auto& lTerms = lVector->terms();


            if( lTerms.empty() )

            {
                co_yield { lhs, tcc };

                co_return;

            }

            Vector sol;
            co_yield HalfUnifyVectors( lTerms, 0, sol, tcc );
        } );

        // 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.addUnificationRule( TCRINFOS, VECOFLENGTH( VL ), []( const Term& lhs, const Term& rhs, const TypeCheckingContext& tcc ) -> TCGen

#include "sema.h"

namespace goose::sema
{
    void SetupHoleUnificationRules( TypeCheckingRuleSet& ruleSet )
    {
        // Anonymous hole half-unification: add 1 to the anon holes count,
        // yield the hole as is.
        ruleSet.addHalfUnificationRule( TCRINFOS,
            HOLE( "_"_sid ),
        []( const Term& lhs, TypeCheckingContext tcc ) -> TCGen
        {
            tcc.addAnonymousHole();
            co_yield { lhs, tcc };
        } );

        // Anonymous hole versus anything: add 1 to the anon holes count,
        // yield the half unification of the rhs
        ruleSet.addUnificationRule( TCRINFOS,
            HOLE( "_"_sid ),
            ANYTERM( _ ),
        []( const Term& lhs, const Term& rhs, TypeCheckingContext tcc ) -> TCGen
        {
            tcc.addAnonymousHole();

            for( auto&& [s,tcc] : HalfUnify( rhs, tcc.flip() ) )
                co_yield { s, tcc.flip() };
        } );

        // Hole half-unification: Convert it to a numbered hole,
        // If the name wasn't already known, add 1 to the score's unique holes count.
        ruleSet.addHalfUnificationRule( TCRINFOS,
            HolePattern(),
        []( const Term& lhs, TypeCheckingContext tcc ) -> TCGen
        {
            auto lh = *HoleFromIRExpr( lhs );

            if( !lh.name.isNumerical() )
            {
                // This is a named hole: look up its name.
                auto holeIndex = tcc.getLHSHoleIndex( lh.name );
                if( holeIndex != TypeCheckingContext::InvalidIndex )
                {
                    if( !tcc.isHoleLocked( holeIndex ) )
                        co_yield { HOLE( StringId( holeIndex ) ), tcc };
                }
                else
                {
                    // This is a new name: create a new value,
                    // and increment the number of unique holes in the current score.
                    auto index = tcc.createValue();
                    tcc.setLHSHoleIndex( lh.name, index );
                    co_yield { HOLE( StringId( index ) ), tcc };
                }
            }
            else
            {
                // This is already an indexed hole: yield it as is.
                if( !tcc.isHoleLocked( lh.name.id() ) )
                    co_yield { lhs, tcc };
            }


        } );

        // Hole vs anything
        ruleSet.addUnificationRule( TCRINFOS,
            HolePattern(),
            ANYTERM( _ ),
        []( const Term& lhs, const Term& rhs, TypeCheckingContext tcc ) -> TCGen

                if( index == TypeCheckingContext::InvalidIndex )
                {
                    // This is a new name: create a new value.
                    index = tcc.createValue();
                    tcc.setLHSHoleIndex( h.name, index );
                    auto holeExpr = HOLE( StringId( index ) );

                    for( auto&& [e,tcc] : HalfUnify( rhs, tcc.flip() ) )
                    {
                        tcc.setValue( index, SetComplexity( move( e ), tcc.complexity() - oldComplexity ) );
                        co_yield { move( holeExpr ), tcc.flip() };
                    }

                    co_return;
                }
            }

                    tcc.unlockHole( index );
                    tcc.setValue( index, SetComplexity( move( e ), tcc.complexity() - oldComplexity ) );
                    co_yield { move( holeExpr ), tcc };
                }
            }
            else
            {
                for( auto&& [e,tcc] : HalfUnify( rhs, tcc.flip() ) )
                {
                    tcc.unlockHole( index );
                    tcc.setValue( index, SetComplexity( move( e ), tcc.complexity() - oldComplexity ) );
                    co_yield { move( holeExpr ), tcc.flip() };
                }
            }
        } );

        // Hole vs hole
        ruleSet.addUnificationRule( TCRINFOS,

            // stored in the other one. We can't just copy the value over as we would lose the dependency
            // relationship between the two holes.
            const auto& lval = tcc.getValue( lindex );
            const auto& rval = tcc.getValue( rindex );

            if( !rval )
            {
                for( auto&& [e,tcc] : HalfUnify( *lval, tcc ) )
                {
                    tcc.unlockHole( lindex );
                    tcc.unlockHole( rindex );

                    tcc.setValue( rindex, HOLE( StringId( lindex ) ) );
                    co_yield { HOLE( StringId( lindex ) ), tcc };
                }
                co_return;
            }

            if( !lval )
            {
                for( auto&& [e,tcc] : HalfUnify( *rval, tcc.flip() ) )
                {
                    tcc.unlockHole( lindex );
                    tcc.unlockHole( rindex );

                    tcc.setValue( lindex, HOLE( StringId( rindex ) ) );
                    co_yield { HOLE( StringId( rindex ) ), tcc.flip() };
                }

        auto&& [quoted] = *result;
        return quoted;
    }

    void SetupQuoteUnificationRules( TypeCheckingRuleSet& ruleSet )
    {
        ruleSet.addHalfUnificationRule( TCRINFOS, VEC( TSID( quote ), ANYTERM( _ ) ),
            []( const Term& lhs, const TypeCheckingContext& tcc ) -> TCGen
            {
                co_yield { lhs, tcc };
            } );

        ruleSet.addUnificationRule( TCRINFOS, VEC( TSID( quote ), ANYTERM( _ ) ),
            []( const Term& lhs, const Term& rhs, const TypeCheckingContext& tcc ) -> TCGen
            {
                if( lhs == rhs )
                    co_yield { lhs, tcc };