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
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
|
#include "sema.h"
namespace empathy::sema
{
Term Mk3WayUnificationTerm( const Term& term1, const Term& term2 )
{
return TVEC( TSID( uni ), term1, term2 );
}
3Way( const Term& lhs, const Term& rhs, UnificationContext& c )
auto result = Decompose( lhs,
Vec(
Lit( "uni"_sid ),
SubTerm(),
SubTerm()
)
);
assert( result );
auto&& [t1,t2] = *result;
for( auto&& [u,c] : Unify( t1, t2, c ) )
{
auto localC = c;
localC.setRHSNamespaceIndex( savedRHSNamespaceIndex );
co_yield Unify( u, rhs, localC );
}
}
void Setup3WayUnificationRules( UnificationRuleSet& ruleSet )
{
ruleSet.addHalfUnificationRule( TVEC( TSID( uni ), ANYTERM( _ ), ANYTERM( _ ) ),
[]( const Term& lhs, UnificationContext& c ) -> UniGen
{
auto result = Decompose( lhs,
Vec(
Lit( "uni"_sid ),
SubTerm(),
SubTerm()
)
);
assert( result );
auto&& [t1,t2] = *result;
for( auto&& [u,c] : Unify( t1, t2, c ) )
{
auto localC = c;
localC.setRHSNamespaceIndex( savedRHSNamespaceIndex );
co_yield { u, localC };
}
} );
ruleSet.addSymRule( TVEC( TSID( uni ), ANYTERM( _ ), ANYTERM( _ ) ), ANYTERM( _ ), Unify3Way );
ruleSet.addSymRule( TVEC( TSID( uni ), ANYTERM( _ ), ANYTERM( _ ) ), Unify3Way );
}
}
|
|
|
<
<
<
<
<
|
<
<
<
<
<
<
<
|
|
<
|
|
>
>
|
<
<
<
<
<
<
<
|
|
<
|
|
|
|
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
|
#include "builtins/builtins.h"
namespace empathy::builtins
{
UniGen UnifyTDecl( const Term& lhs, const Term& rhs, UnificationContext& c )
{
auto tdecl = FromValue< TDecl >( *ValueFromIRExpr( lhs ) );
assert( tdecl );
// Both of the expressions are side by side in the same input expresion, which
// means their hole names share the same namespace. So pretend that both the LHS and RHS
// namespaces are the same for their unification, but restore it after.
auto savedRHSNamespaceIndex = c.RHSNamespaceIndex();
c.setRHSNamespaceIndex( c.LHSNamespaceIndex() );
for( auto&& [u,c] : Unify( tdecl->type(), tdecl->value(), c ) )
{
auto localC = c;
localC.setRHSNamespaceIndex( savedRHSNamespaceIndex );
co_yield Unify( u, rhs, localC );
}
}
void SetupTDeclUnification( Env& e )
{
auto tDeclPat = ValueToIRExpr( Value( GetValueType< TDecl >(), TVEC( ANYTERM( _ ), ANYTERM( _ ) ) ) );
e.unificationRuleSet()->addHalfUnificationRule( tDeclPat,
[]( const Term& lhs, UnificationContext& c ) -> UniGen
{
auto tdecl = FromValue< TDecl >( *ValueFromIRExpr( lhs ) );
assert( tdecl );
// Both of the expressions are side by side in the same input expression, which
// means their hole names share the same namespace. So pretend that both the LHS and RHS
// namespaces are the same for their unification, but restore it after.
auto savedRHSNamespaceIndex = c.RHSNamespaceIndex();
c.setRHSNamespaceIndex( c.LHSNamespaceIndex() );
for( auto&& [u,c] : Unify( tdecl->type(), tdecl->value(), c ) )
{
auto localC = c;
localC.setRHSNamespaceIndex( savedRHSNamespaceIndex );
co_yield { u, localC };
}
} );
e.unificationRuleSet()->addSymRule( tDeclPat, ANYTERM( _ ), UnifyTDecl );
e.unificationRuleSet()->addSymRule( tDeclPat, UnifyTDecl );
}
}
|