Goose  Artifact [8fab356cf9]

Artifact 8fab356cf98c2b2c6acc04de86abe7a950c292ae244c8572ff01e14250a7b123:

• File bs/builtins/types/predicates/predicates.cpp — part of check-in [1fe5a1ac2b] at 2021-10-31 18:52:16 on branch trunk —
  • Reverted most of the horribly complicated changes done since [b3ff9af3c2fe4925], other than the ability to hash all terms, values, instructions and predicates
  • Solved the problem for which tests were added in [b3ff9af3c2fe4925] in a much simpler way
  (user: zlodo size: 3624)

#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();
    }

    Term AppendPredicatesHashToIdentity( const Term& identity, uint64_t hash )
    {
        return AppendToVectorTerm( identity, VEC( TSID( pred_hash ), hash ) );
    }

    Term StripPredicateHashesFromIdentity( const Term& identity )
    {
        const auto& vec = *get< pvec >( identity );
        auto result = make_shared< Vector >();
        result->reserve( vec.terms().size() );

        for( auto&& t : vec.terms() )
        {
            auto decomp = Decompose( t,
                Vec(
                    Lit( "pred_hash"_sid ),
                    Val< uint64_t >()
                )
            );

            if( decomp )
                continue;

            const auto* pNestedVec = get_if< pvec >( &t );
            if( pNestedVec )
                result->append( StripPredicateHashesFromIdentity( t ) );
            else
                result->append( t );
        }

        return result;
    }
}