Goose  Artifact [2631112e87]

Artifact 2631112e87352bbffc048e05f74ed86b388f62139f420714324d97a4891d7c78:

• File bs/builtins/types/predicates/predicates.cpp — part of check-in [2d2defb442] at 2021-08-29 21:49:39 on branch trunk —
  • Type predicates' identity and placeholder are now created immediately, rather than when parsing their content
  • Added missing type predicates lazy parsing during typechecking
  • Fixed a type checking rule falling back to unification, which is no longer needed
  (user: achavasse size: 2701)

#include "builtins/builtins.h"
#include "lex/lex.h"
#include "parse/parse.h"
#include "builtins/helpers.h"

using namespace goose::parse;

namespace goose::builtins
{
    const Term& EmptyPredicates()
    {
        static auto ep = VEC( TSID( predicates ), TERM( ptr< void >() ) );
        return ep;
    }

    optional< ptr< TypePredicates > > GetTypePredicates( const Value& t )
    {
        if( !t.isType() )
            return nullopt;

        auto vec = Decompose( t.val(),
            Val< pvec >()
        );

        if( !vec )
            return nullopt;

        if( vec->get()->terms().size() < 3 )
            return nullopt;

        auto result = Decompose( vec->get()->terms()[1],
            Vec(
                Lit( "predicates"_sid ),
                Val< ptr< void > >()
            )
        );

        if( !result )
            return nullopt;

        auto&& [pt] = *result;
        return static_pointer_cast< TypePredicates >( pt );
    }

    Term InjectPredicatesIntoStdType( const Term& t, const ptr< TypePredicates >& predicates )
    {
        Term result( t );

        auto vec = Decompose( t,
            Val< pvec >()
        );

        assert( vec );
        assert( vec->get()->terms().size() >= 3 );

        vec->get()->terms()[1] = VEC( TSID( predicates ), static_pointer_cast< void >( predicates ) );
        return result;
    }

    bool ParseTypePredicates( const Context& c, const Value& type )
    {
        auto optTypePreds = GetTypePredicates( type );
        if( !optTypePreds || !*optTypePreds )
            return true;

        auto& tp = **optTypePreds;
        return ParseTypePredicates( c, tp );
    }

    bool ParseTypePredicates( const Context& c, TypePredicates& tp )
    {
        if( tp.m_unparsedPredicates.empty() )
            return true;

        Context localContext( c.env(), tp.m_identity );

        for( auto&& toks : tp.m_unparsedPredicates )
        {
            auto tokProvider = lex::MakeVectorAdapter( toks );
            auto r = make_shared< parse::Resolver >( tokProvider, localContext );
            Parser p( r );

            if( !ParseExpressionList( p, precedence::VerificationPredicate + 1, tp.m_predicates ) )
            {
                tp.m_unparsedPredicates.clear();
                return false;
            }
        }

        tp.m_unparsedPredicates.clear();

        // Context isn't relevant for unsatisfiable conditions errors.
        DiagnosticsContext dc( 0, true );

        // verify that the verification statements are satisfiable
        verify::Condition vsv( c );
        if( !vsv.addConditionsList( tp.m_predicates ) )
            return false;

        return vsv.verify();
    }
}