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