Goose  Check-in [121c78d7e5]

Many hyperlinks are disabled.
Use anonymous login to enable hyperlinks.

Overview
Comment:sema: implemented SubstituteNamed.
Downloads: Tarball | ZIP archive
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA3-256: 121c78d7e5a9ebc7292a5fa7848cbb138d290db1b653d42029ecf5586170eafd
User & Date: achavasse 2019-04-01 20:37:04.710
Context
2019-04-02
20:38
Higher order polymorphism: implemented ConstrainedFunc unification. check-in: f6c1df5107 user: achavasse tags: trunk
2019-04-01
20:37
sema: implemented SubstituteNamed. check-in: 121c78d7e5 user: achavasse tags: trunk
20:25
Higher order polymorphism: implemented ConstrainedFunc invocation rule. check-in: 01c479df9a user: achavasse tags: trunk
Changes
Unified Diff Ignore Whitespace Patch
Changes to bs/sema/substitute.cpp.
42
43
44
45
46
47
48









































49
50
51
52
            auto newT = Substitute( t, context );
            if( !newT )
                return nullopt;

            faulty = faulty || newT->isFaulty();
            vt.push_back( move( *newT ) );
        }










































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







>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>




42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
            auto newT = Substitute( t, context );
            if( !newT )
                return nullopt;

            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;

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

            // 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 );
        }

        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 ) );
    }
}
Changes to bs/sema/substitute.h.
1
2
3
4
5
6

7
8
9
#ifndef EMPATHY_SEMA_SUBSTITUTE_H
#define EMPATHY_SEMA_SUBSTITUTE_H

namespace empathy::sema
{
    extern optional< Term > Substitute( const Term& src, const UnificationContext& context );

}

#endif






>



1
2
3
4
5
6
7
8
9
10
#ifndef EMPATHY_SEMA_SUBSTITUTE_H
#define EMPATHY_SEMA_SUBSTITUTE_H

namespace empathy::sema
{
    extern optional< Term > Substitute( const Term& src, const UnificationContext& context );
    extern Term SubstituteNamed( const Term& src, const UnificationContext& context );
}

#endif