1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
|
#include "sema.h"
namespace empathy::sema
{
Term Substitute( const Term& src, const UnificationContext& context )
{
if( !holds_alternative< pvec >( src.content() ) )
return src;
auto optHole = HoleFromIRExpr( src );
if( optHole )
{
const auto& hole = *optHole;
// We only substitute indexed holes. If we encounter a named hole,
// output it as is.
if( !holds_alternative< uint32_t >( hole ) )
return src;
const auto& optVal = context.getValue( get< uint32_t >( hole ) );
if( !optVal )
return src;
return Substitute( *optVal, 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 = Substitute( t, context );
faulty = faulty || newT.isFaulty();
vt.push_back( move( newT ) );
}
return Term( src.location(), make_shared< Vector >( vt.persistent(), faulty ) );
}
}
|
|
|
<
>
>
>
>
>
>
>
>
>
>
>
>
|
|
|
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
|
#include "sema.h"
namespace empathy::sema
{
optional< Term > Substitute( 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 indexed holes. If we encounter a named hole,
// output it as is.
if( !holds_alternative< uint32_t >( hole ) )
return src;
const auto& optVal = context.getValue( get< uint32_t >( hole ) );
if( !optVal )
return src;
return Substitute( *optVal, context );
}
if( auto optCB = UnwrapCallback( src ) )
{
auto val = Substitute( optCB->first, context );
if( !val )
return nullopt;
return ( *optCB->second )( *val );
}
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 = 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 ) );
}
}
|