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
|
#include "builtins/builtins.h"
namespace empathy::builtins
{
Term BuildArgPatternFromTDecl( const TDecl& td )
{
return ValueToIRExpr( ValuePattern( MkHole( "_"_sid ), td.type(), MkHole( "_"_sid ) ) );
}
UniGen UnifyTDecl( const Term& lhs, const Term& rhs, UnificationContext& c )
{
auto tdecl = FromValue< TDecl >( *ValueFromIRExpr( lhs ) );
assert( tdecl );
auto tdeclHole = MkHole( tdecl->name() );
auto pat = ValueToIRExpr( Value( tdecl->type(), MkHole( "_"_sid ) ) );
for( auto&& [s,c] : Unify( pat, rhs, c ) )
{
// We need to unify the result with a hole named after the decl. However, since both sides of
// this unification orignally appeared on the LHS, we need to setup RHS to alias the LHS namespace for this.
auto savedRHSNamespaceIndex = c.RHSNamespaceIndex();
c.setRHSNamespaceIndex( c.LHSNamespaceIndex() );
for( auto&& [s,c] : Unify( s, tdeclHole, c ) )
{
auto localC = c;
localC.setRHSNamespaceIndex( savedRHSNamespaceIndex );
co_yield { s, localC };
}
c.setRHSNamespaceIndex( savedRHSNamespaceIndex );
}
}
void SetupTDeclUnification( Env& e )
{
auto tDeclPat = ValueToIRExpr( Value( GetValueType< TDecl >(), TVEC( ANYTERM( _ ), ANYTERM( _ ) ) ) );
|
|
>
>
>
>
>
>
>
|
|
|
>
>
>
|
|
|
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
|
#include "builtins/builtins.h"
namespace empathy::builtins
{
Term BuildArgPatternFromTDecl( const TDecl& td )
{
return ValueToIRExpr( ValuePattern( MkHole( "_"_sid ), td.type(), MkHole( "_"_sid ) ) );
}
UniGen UnifyTDecl( const Term& lhs, const Term& rhs, UnificationContext& uc )
{
auto tdecl = FromValue< TDecl >( *ValueFromIRExpr( lhs ) );
assert( tdecl );
auto tdeclHole = MkHole( tdecl->name() );
auto pat = ValueToIRExpr( Value( tdecl->type(), MkHole( "_"_sid ) ) );
// We are replacing lhs with a different terms and re-unifying,
// so update the complexity accordingly. The structure of the tdecl
// shouldn't count, only its pattern.
uc.subComplexity( GetComplexity( lhs ) );
uc.addComplexity( GetComplexity( pat ) );
for( auto&& [s,uc] : Unify( pat, rhs, uc ) )
{
// We need to unify the result with a hole named after the decl. However, since both sides of
// this unification orignally appeared on the LHS, we need to setup RHS to alias the LHS namespace for this.
auto savedRHSNamespaceIndex = uc.RHSNamespaceIndex();
uc.setRHSNamespaceIndex( uc.LHSNamespaceIndex() );
uc.subComplexity( GetComplexity( pat ) + GetComplexity( rhs ) );
uc.addComplexity( GetComplexity( s ) );
for( auto&& [s,c] : Unify( s, tdeclHole, uc ) )
{
auto localC = c;
localC.setRHSNamespaceIndex( savedRHSNamespaceIndex );
co_yield { s, localC };
}
uc.setRHSNamespaceIndex( savedRHSNamespaceIndex );
}
}
void SetupTDeclUnification( Env& e )
{
auto tDeclPat = ValueToIRExpr( Value( GetValueType< TDecl >(), TVEC( ANYTERM( _ ), ANYTERM( _ ) ) ) );
|
85
86
87
88
89
90
91
92
93
94
95
96
97
98
|
// Create a new named hole namespace to isolate holes from the passed function from those in
// the called function.
auto savedRHSNamespaceIndex = uc.RHSNamespaceIndex();
uc.setRHSNamespaceIndex( uc.newNamespaceIndex() );
auto oldValueRequired = uc.isValueResolutionRequired();
uc.setValueResolutionRequired( false );
for( auto&& [s, uc] : Unify( callPat, rhs, uc ) )
{
// Restore the namespace
auto localC = uc;
localC.setRHSNamespaceIndex( savedRHSNamespaceIndex );
localC.setValueResolutionRequired( oldValueRequired );
|
>
>
>
>
>
>
|
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
|
// Create a new named hole namespace to isolate holes from the passed function from those in
// the called function.
auto savedRHSNamespaceIndex = uc.RHSNamespaceIndex();
uc.setRHSNamespaceIndex( uc.newNamespaceIndex() );
auto oldValueRequired = uc.isValueResolutionRequired();
uc.setValueResolutionRequired( false );
// We are replacing lhs with a different terms and re-unifying,
// so update the complexity accordingly. The structure of the tdecl
// shouldn't count, only its pattern.
uc.subComplexity( GetComplexity( lhs ) );
uc.addComplexity( GetComplexity( callPat ) );
for( auto&& [s, uc] : Unify( callPat, rhs, uc ) )
{
// Restore the namespace
auto localC = uc;
localC.setRHSNamespaceIndex( savedRHSNamespaceIndex );
localC.setValueResolutionRequired( oldValueRequired );
|
145
146
147
148
149
150
151
152
153
154
155
156
157
158
|
// Create a new named hole namespace to isolate holes from the passed function from those in
// the called function.
auto savedRHSNamespaceIndex = uc.RHSNamespaceIndex();
uc.setRHSNamespaceIndex( uc.newNamespaceIndex() );
auto oldValueRequired = uc.isValueResolutionRequired();
uc.setValueResolutionRequired( false );
for( auto&& [s, uc] : Unify( callPat, rhs, uc ) )
{
// Restore the namespace
auto localC = uc;
localC.setRHSNamespaceIndex( savedRHSNamespaceIndex );
localC.setValueResolutionRequired( oldValueRequired );
|
>
>
>
>
>
>
|
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
|
// Create a new named hole namespace to isolate holes from the passed function from those in
// the called function.
auto savedRHSNamespaceIndex = uc.RHSNamespaceIndex();
uc.setRHSNamespaceIndex( uc.newNamespaceIndex() );
auto oldValueRequired = uc.isValueResolutionRequired();
uc.setValueResolutionRequired( false );
// We are replacing lhs with a different terms and re-unifying,
// so update the complexity accordingly. The structure of the tdecl
// shouldn't count, only its pattern.
uc.subComplexity( GetComplexity( lhs ) );
uc.addComplexity( GetComplexity( callPat ) );
for( auto&& [s, uc] : Unify( callPat, rhs, uc ) )
{
// Restore the namespace
auto localC = uc;
localC.setRHSNamespaceIndex( savedRHSNamespaceIndex );
localC.setValueResolutionRequired( oldValueRequired );
|