Goose  Artifact [b6394901bf]

Artifact b6394901bf998a13c3f5dd0123414de32c90f5c70b260b92ad3ae06f34b6a694:

• File bs/builtins/statements/verification.cpp — part of check-in [1ad61a2717] at 2021-11-11 20:05:58 on branch trunk — Refactored the code builder: it is now carried around as a Value, and accessed through a bunch of extension points, so we can have different builders (and even user defined ones) later to make classes etc. (user: zlodo size: 2998)

#include "builtins/builtins.h"
#include "precedence.h"

using namespace goose;
using namespace goose::eir;
using namespace goose::parse;
using namespace goose::builtins;

namespace
{
    optional< uint32_t > VerifStmtPrecedence( const Parser& p )
    {
        auto lastVal = p.peekLastValue();
        if( !lastVal )
            return nullopt;

        if( !IsFuncType( *lastVal ) && !IsTFuncType( *lastVal ) )
            return nullopt;

        return precedence::VerificationPredicate;
    }

    template< typename F >
    bool ParseVerifStmt( Parser& p, LocationId locationId, uint32_t prec, const char* name, F&& func )
    {
        auto& dm = DiagnosticsManager::GetInstance();

        auto type = p.peekLastValue();
        if( !type )
            return false;

        auto delim = p.resolver()->lookAheadUnresolved();
        if( !delim )
        {
            dm.emitSyntaxErrorMessage( p.resolver()->currentLocation(), format( "'[' expected after '{}'.", name ), 0 );
            return false;
        }

        auto decomp = Decompose( delim->first, Val< Delimiter >() );
        if( !decomp || *decomp != Delimiter::OpenBracket )
        {
            dm.emitSyntaxErrorMessage( p.resolver()->currentLocation(), format( "'[' expected after '{}'.", name ), 0 );
            return false;
        }

        ptr< vector< TermLoc > > tokList;

        if( auto ft = FromValue< FuncType >( *type ) )
            tokList = func( *ft );
        else if( auto tft = FromValue< TFuncType >( *type ) )
            tokList = func( *tft );
        else
            return false;

        auto g = p.resolver()->consumeUnit();

        // Strip the start and end brackets
        auto beg = g.begin();
        advance( beg, 1 );
        move( beg, g.end(), back_inserter( *tokList ) );
        tokList->resize( tokList->size() - 1 );

        return true;
    }

    bool ParseRequiresStmt( Parser& p, LocationId locationId, uint32_t prec )
    {
        return ParseVerifStmt( p, locationId, prec, "requires", [&]< typename FT >( FT& ft )
        {
            if constexpr( is_same_v< FT, FuncType > )
            {
                return ft.verifInfos()->preCondToks();
            }
            else
            {
                return ft.preCondToks();
            }
        } );
    }

    bool ParseEnsuresStmt( Parser& p, LocationId locationId, uint32_t prec )
    {
        return ParseVerifStmt( p, locationId, prec, "ensures", [&]< typename FT >( FT& ft )
        {
            if constexpr( is_same_v< FT, FuncType > )
            {
                return ft.verifInfos()->postCondToks();
            }
            else
            {
                return ft.postCondToks();
            }
        } );
    }
}

namespace goose::builtins
{
    void SetupVerificationStmts( Env& e )
    {
        RegisterRule( e, "requires"_sid, Rule( VerifStmtPrecedence, ParseRequiresStmt ) );
        RegisterRule( e, "ensures"_sid, Rule( VerifStmtPrecedence, ParseEnsuresStmt ) );
    }
}