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
|
localC.setRHSNamespaceIndex( savedRHSNamespaceIndex );
co_yield Unify( u, rhs, localC );
}
}
void Setup3WayUnificationRules( UnificationRuleSet& ruleSet )
{
ruleSet.addHalfUnificationRule( TVEC( TSID( _ ), ANYTERM( _ ), ANYTERM( _ ) ),
[]( const Term& lhs, UnificationContext& c ) -> UniGen
{
auto result = Decompose( lhs,
Vec(
Lit( "uni"_sid ),
SubTerm(),
SubTerm()
)
);
assert( result );
auto&& [t1,t2] = *result;
// 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( t1, t2, c ) )
{
auto localC = c;
localC.setRHSNamespaceIndex( savedRHSNamespaceIndex );
co_yield { u, localC };
}
} );
ruleSet.addSymRule( TVEC( TSID( _ ), ANYTERM( _ ), ANYTERM( _ ) ), ANYTERM( _ ), Unify3Way );
ruleSet.addSymRule( TVEC( TSID( _ ), ANYTERM( _ ), ANYTERM( _ ) ), Unify3Way );
}
}
|
|
|
|
|
|
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
|
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;
// 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( 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 );
}
}
|